BanLat/Substructures/Band/Lattice.lean
All source files · Download exact source
SHA-256: 8a9f48e31362404d21f04fc4a43ed10de79e08ec5f37cf890132ae7ac48d8290
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Band.Basic67/-!8# The lattice of bands910The collection of bands of a vector lattice `X`, ordered by inclusion, forms a11complete lattice. It contains the whole space `⊤ = X`, the trivial band12`⊥ = {0}`, and is closed under arbitrary intersections; binary infima are13given by intersection.14-/1516variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]17 [VectorLattice X]1819namespace Band2021/-! ### The order on bands -/2223/-- Bands of `X`, ordered by inclusion, form a partial order. -/24instance : PartialOrder (Band X) := .ofSetLike (Band X) X2526/-! ### Arbitrary intersections, top and bottom -/2728/-- Arbitrary intersections of bands are bands. -/29instance : InfSet (Band X) where30 sInf S :=31 { toOrderIdeal := sInf ((·.toOrderIdeal) '' S)32 sSup_mem' := by33 intro T hTsub hne x hx34 refine OrderIdeal.mem_sInf.mpr ?_35 rintro _ ⟨B, hB, rfl⟩36 refine B.sSup_mem (fun s hs => ?_) hne hx37 exact OrderIdeal.mem_sInf.mp (hTsub hs) _ ⟨B, hB, rfl⟩ }3839@[simp] theorem mem_sInf {S : Set (Band X)} {x : X} :40 x ∈ (sInf S : Band X) ↔ ∀ B ∈ S, x ∈ B := by41 change x ∈ (sInf ((·.toOrderIdeal) '' S) : OrderIdeal X) ↔ _42 rw [OrderIdeal.mem_sInf]43 exact ⟨fun h B hB => h _ ⟨B, hB, rfl⟩,44 by rintro h _ ⟨B, hB, rfl⟩; exact h B hB⟩4546/-- The whole space `X` is a band. -/47instance : Top (Band X) where48 top :=49 { toOrderIdeal := ⊤50 sSup_mem' := fun _ _ _ _ _ => OrderIdeal.mem_top }5152@[simp] theorem mem_top {x : X} : x ∈ (⊤ : Band X) := Submodule.mem_top5354/-- The trivial band `{0}` is a band. -/55instance : Bot (Band X) where56 bot :=57 { toOrderIdeal := ⊥58 sSup_mem' := by59 intro S hSsub hne x hx60 obtain ⟨s₀, hs₀⟩ := hne61 have hs₀_eq : s₀ = 0 := OrderIdeal.mem_bot.mp (hSsub hs₀)62 have hub : x ≤ 0 :=63 hx.2 (fun s hs => by64 rw [OrderIdeal.mem_bot.mp (hSsub hs)])65 have hlb : 0 ≤ x := by66 have h := hx.1 hs₀; rwa [hs₀_eq] at h67 exact OrderIdeal.mem_bot.mpr (le_antisymm hub hlb) }6869@[simp] theorem mem_bot {x : X} : x ∈ (⊥ : Band X) ↔ x = 0 :=70 Submodule.mem_bot ℝ7172/-! ### The complete lattice of bands -/7374/-- Bands of `X`, ordered by inclusion, form a complete lattice. Arbitrary75infima are given by intersection, the bottom element is the trivial band76`{0}`, and the top element is the whole space. -/77instance : CompleteLattice (Band X) where78 __ := (inferInstance : PartialOrder (Band X))79 sup B₁ B₂ := sInf {K : Band X | B₁ ≤ K ∧ B₂ ≤ K}80 inf B₁ B₂ :=81 { toOrderIdeal := B₁.toOrderIdeal ⊓ B₂.toOrderIdeal82 sSup_mem' := by83 intro S hSsub hne x hx84 refine ⟨B₁.sSup_mem (fun s hs => (hSsub hs).1) hne hx,85 B₂.sSup_mem (fun s hs => (hSsub hs).2) hne hx⟩ }86 top := ⊤87 bot := ⊥88 sInf := sInf89 sSup S := sInf {K : Band X | ∀ B ∈ S, B ≤ K}90 le_top := fun _ _ _ => Submodule.mem_top91 bot_le := fun B x hx => by92 rw [mem_bot.mp hx]; exact B.toOrderIdeal.toSubmodule.zero_mem93 le_sup_left := fun B₁ _ x hx => by94 rw [mem_sInf]; rintro K ⟨h₁, _⟩; exact h₁ hx95 le_sup_right := fun _ B₂ x hx => by96 rw [mem_sInf]; rintro K ⟨_, h₂⟩; exact h₂ hx97 sup_le := fun B₁ B₂ K h₁ h₂ x hx => by98 rw [mem_sInf] at hx; exact hx K ⟨h₁, h₂⟩99 inf_le_left := fun _ _ _ hx => hx.1100 inf_le_right := fun _ _ _ hx => hx.2101 le_inf := fun _ _ _ h₁ h₂ _ hx => ⟨h₁ hx, h₂ hx⟩102 isLUB_sSup := fun S => by103 refine ⟨?_, ?_⟩104 · intro J hJ x hx105 rw [mem_sInf]106 intro K hK107 exact hK J hJ hx108 · intro J hJ x hx109 rw [mem_sInf] at hx110 exact hx J hJ111 isGLB_sInf := fun S => by112 refine ⟨?_, ?_⟩113 · intro J hJ x hx114 rw [mem_sInf] at hx115 exact hx J hJ116 · intro J hJ x hx117 rw [mem_sInf]118 intro K hK119 exact hJ hK hx120121@[simp] theorem inf_toOrderIdeal (B₁ B₂ : Band X) :122 (B₁ ⊓ B₂).toOrderIdeal = B₁.toOrderIdeal ⊓ B₂.toOrderIdeal := rfl123124end Band125