BanLat/Substructures/Band/Basic.lean

All source files · Download exact source

SHA-256: d2b215633f9ab3b5327e8648fa0674a281f3598ad565260b2f5c02312f6b4231

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Ideal6import BanLat.OrderComplete78/-!9# Bands1011A **band** in a vector lattice is an order ideal that is **order closed**:12whenever a subset of the band has a supremum in the ambient space, that13supremum also lies in the band.1415This file defines the bundled structure `Band`, relates bands to order ideals16and vector sublattices, proves the basic closure properties, and records that17order completeness passes from the ambient vector lattice to a band.18-/1920section MainVariables21variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]22  [VectorLattice X]2324/-! ### The band structure -/2526/-- A **band** in a vector lattice is an order ideal that is **order closed**:27whenever a subset of the band has a supremum in `X`, that supremum also lies28in the band. -/29structure Band (X : Type*) [AddCommGroup X] [Lattice X]30    [IsOrderedAddMonoid X] [VectorLattice X]31    extends OrderIdeal X where32  sSup_mem' :33    ∀ (S : Set X), S ⊆ carrier → S.Nonempty → ∀ x, IsLUB S x → x ∈ carrier3435namespace Band3637instance : SetLike (Band X) X where38  coe B := B.carrier39  coe_injective p q h := by40    cases p; cases q; congr41    exact SetLike.ext' h4243variable (B : Band X)4445/-! ### A band is an ideal and a vector sublattice -/4647/-- Every band is an order ideal. -/48def toOrderIdeal' : OrderIdeal X := B.toOrderIdeal4950/-! ### Closure under suprema -/5152/-- A band is closed under suprema: if a subset of the band has a supremum in53`X`, the supremum lies in the band. -/54theorem sSup_mem {S : Set X} (hS : S ⊆ (B : Set X)) (hne : S.Nonempty)55    {x : X} (hx : IsLUB S x) : x ∈ B :=56  B.sSup_mem' S hS hne x hx5758/-! ### Basic membership lemmas inherited from the underlying ideal -/5960/-- A band is closed under `⊔`. -/61theorem sup_mem {x y : X} (hx : x ∈ B) (hy : y ∈ B) :62    x ⊔ y ∈ B :=63  B.toOrderIdeal.sup_mem hx hy6465/-- A band is closed under `⊓`. -/66theorem inf_mem {x y : X} (hx : x ∈ B) (hy : y ∈ B) :67    x ⊓ y ∈ B :=68  B.toOrderIdeal.inf_mem hx hy6970/-- A band is solid. -/71theorem solid {x y : X} (hx : x ∈ B) (hy0 : 0 ≤ y) (hyx : y ≤ x) :72    y ∈ B :=73  B.toOrderIdeal.solid hx hy0 hyx7475/-- A band is closed under absolute value. -/76theorem abs_mem {x : X} (hx : x ∈ B) : |x| ∈ B :=77  B.toOrderIdeal.abs_mem hx7879/-- Membership in a band is equivalent to membership of the absolute value. -/80theorem mem_of_abs_mem {x : X} (h : |x| ∈ B) : x ∈ B :=81  B.toOrderIdeal.mem_of_abs_mem h8283/-- Solidity in terms of absolute value. -/84theorem mem_of_abs_le_abs {x y : X} (hx : x ∈ B) (h : |y| ≤ |x|) :85    y ∈ B :=86  B.toOrderIdeal.mem_of_abs_le_abs hx h8788/-! ### Construction from the positive directed closure condition8990It suffices to test the closure condition on positive directed subsets:91an order ideal closed under suprema of positive directed subsets is92automatically a band. -/9394/-- An order ideal is a band as soon as every directed subset of positive95elements with supremum in `X` has its supremum in the ideal. -/96def ofPosDirectedSSupMem (J : OrderIdeal X)97    (h : ∀ S, S ⊆ (J : Set X) → (∀ x ∈ S, 0 ≤ x) → DirectedOn (· ≤ ·) S98      → S.Nonempty → ∀ x, IsLUB S x → x ∈ J) : Band X where99  toOrderIdeal := J100  sSup_mem' := by101    classical102    intro S hSJ hne y hy103    obtain ⟨s₀, hs₀⟩ := hne104    have hs₀J : s₀ ∈ J := hSJ hs₀105    have finsup_mem : ∀ (F : Finset X) (hF : F.Nonempty), ↑F ⊆ S →106        F.sup' hF id ∈ J := by107      intro F hF hFS108      induction hF using Finset.Nonempty.cons_induction with109      | singleton x =>110        rw [Finset.sup'_singleton]111        exact hSJ (hFS (by simp))112      | cons x F hxF hFne ih =>113        rw [Finset.sup'_cons hFne id]114        refine J.sup_mem (hSJ (hFS ?_)) (ih ?_)115        · simp116        · intro a ha; exact hFS (by simp [ha])117    set T : Set X :=118      { z | ∃ F : Finset X, ∃ hF : F.Nonempty, ↑F ⊆ S ∧ s₀ ∈ F ∧119        z = F.sup' hF id - s₀ }120    have hT_J : T ⊆ (J : Set X) := by121      rintro z ⟨F, hF, hFS, _, rfl⟩122      exact J.toSubmodule.sub_mem (finsup_mem F hF hFS) hs₀J123    have hT_pos : ∀ z ∈ T, 0 ≤ z := by124      rintro z ⟨F, hF, hFS, hs₀F, rfl⟩125      exact sub_nonneg.mpr (Finset.le_sup' id hs₀F)126    have hT_dir : DirectedOn (· ≤ ·) T := by127      rintro a ⟨Fa, hFa, hFaS, hs₀a, rfl⟩ b ⟨Fb, hFb, hFbS, hs₀b, rfl⟩128      refine ⟨(Fa ∪ Fb).sup' (hFa.mono Finset.subset_union_left) id - s₀,129        ⟨Fa ∪ Fb, hFa.mono Finset.subset_union_left, ?_, ?_, rfl⟩, ?_, ?_⟩130      · rw [Finset.coe_union]; exact Set.union_subset hFaS hFbS131      · exact Finset.mem_union.mpr (Or.inl hs₀a)132      · exact sub_le_sub_right133          (Finset.sup'_mono id Finset.subset_union_left hFa) s₀134      · exact sub_le_sub_right135          (Finset.sup'_mono id Finset.subset_union_right hFb) s₀136    have hT_ne : T.Nonempty :=137      ⟨0, ⟨{s₀}, Finset.singleton_nonempty s₀, by138        intro a ha; rw [Finset.coe_singleton, Set.mem_singleton_iff] at ha139        rw [ha]; exact hs₀,140        Finset.mem_singleton_self _, by141        rw [Finset.sup'_singleton]; exact (sub_self s₀).symm⟩⟩142    have hT_lub : IsLUB T (y - s₀) := by143      refine ⟨?_, ?_⟩144      · rintro z ⟨F, hF, hFS, _, rfl⟩145        exact sub_le_sub_right146          (Finset.sup'_le hF id (fun a ha => hy.1 (hFS ha))) s₀147      · intro c hc148        rw [sub_le_iff_le_add]149        apply hy.2150        intro s hs151        have hF : ({s, s₀} : Finset X).Nonempty := ⟨s, by simp⟩152        have hFS : (↑({s, s₀} : Finset X) : Set X) ⊆ S := by153          intro a ha154          rw [Finset.coe_insert, Finset.coe_singleton] at ha155          rcases ha with rfl | rfl156          · exact hs157          · exact hs₀158        have hs₀mem : s₀ ∈ ({s, s₀} : Finset X) := by simp159        have hT_elt : ({s, s₀} : Finset X).sup' hF id - s₀ ∈ T :=160          ⟨_, hF, hFS, hs₀mem, rfl⟩161        have hle : ({s, s₀} : Finset X).sup' hF id - s₀ ≤ c := hc hT_elt162        have hsup_ge : s ≤ ({s, s₀} : Finset X).sup' hF id :=163          Finset.le_sup' id (by simp : s ∈ ({s, s₀} : Finset X))164        have : ({s, s₀} : Finset X).sup' hF id ≤ c + s₀ :=165          sub_le_iff_le_add.mp hle166        exact hsup_ge.trans this167    have hu : y - s₀ ∈ J := h T hT_J hT_pos hT_dir hT_ne (y - s₀) hT_lub168    have hres : y - s₀ + s₀ ∈ J := J.toSubmodule.add_mem hu hs₀J169    change y ∈ J.carrier170    rw [sub_add_cancel] at hres171    exact hres172173end Band174175end MainVariables176177section CCLSubtype178179variable {X : Type*} [AddCommGroup X] [ConditionallyCompleteLattice X]180  [IsOrderedAddMonoid X] [VectorLattice X]181182namespace Band183184/-! ### Order completeness of the underlying subtype -/185186/-- A band in an order complete vector lattice is itself order complete. -/187noncomputable instance instConditionallyCompleteLatticeSubtype188    (B : Band X) :189    ConditionallyCompleteLattice ↥B.toSubmodule := by190  letI : Nonempty ↥B.toSubmodule := ⟨0⟩191  refine conditionallyCompleteLatticeOfPosSet ↥B.toSubmodule ?_192  intro S _ hne hbdd193  set T : Set X := Subtype.val '' S with hT_def194  have hT_sub : T ⊆ (B : Set X) := by195    rintro _ ⟨⟨a, ha⟩, _, rfl⟩; exact ha196  have hT_ne : T.Nonempty := hne.image _197  obtain ⟨u, hu⟩ := hbdd198  have hT_bdd : BddAbove T :=199    ⟨u.1, by rintro _ ⟨v, hv, rfl⟩; exact hu hv⟩200  have hT_lub : IsLUB T (sSup T) := isLUB_csSup hT_ne hT_bdd201  refine ⟨⟨sSup T, B.sSup_mem hT_sub hT_ne hT_lub⟩, ?_, ?_⟩202  · rintro a ha203    change a.1 ≤ sSup T204    exact hT_lub.1 ⟨a, ha, rfl⟩205  · rintro a hub206    change sSup T ≤ a.1207    exact hT_lub.2 (by rintro _ ⟨b, hb, rfl⟩; exact hub hb)208209end Band210211end CCLSubtype212