Complete Sublattices

This file defines complete sublattices. These are subsets of complete lattices which are closed under arbitrary suprema and infima. As a standard example one could take the complete sublattice of invariant submodules of some module with respect to a linear map.

Main definitions:

• CompleteSublattice: the definition of a complete sublattice
• CompleteSublattice.mk': an alternate constructor for a complete sublattice, demanding fewer hypotheses
• CompleteSublattice.instCompleteLattice: a complete sublattice is a complete lattice
• CompleteSublattice.map: complete sublattices push forward under complete lattice morphisms.
• CompleteSublattice.comap: complete sublattices pull back under complete lattice morphisms.

structure CompleteSublattice (α : Type u_1) [CompleteLattice α] extends Sublattice α : Type u_1

A complete sublattice is a subset of a complete lattice that is closed under arbitrary suprema and infima.

• carrier : Set α
• supClosed' : SupClosed self.carrier
• infClosed' : InfClosed self.carrier
• sSupClosed' ⦃s : Set α⦄ : s ⊆ self.carrier → sSup s ∈ self.carrier
• sInfClosed' ⦃s : Set α⦄ : s ⊆ self.carrier → sInf s ∈ self.carrier

def CompleteSublattice.mk' {α : Type u_1} [CompleteLattice α] (carrier : Set α) (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier) (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier) : CompleteSublattice α

To check that a subset is a complete sublattice, one does not need to check that it is closed under binary Sup since this follows from the stronger sSup condition. Likewise for infima.

@[simp]

theorem CompleteSublattice.mk'_carrier {α : Type u_1} [CompleteLattice α] (carrier : Set α) (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier) (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier) : (mk' carrier sSupClosed' sInfClosed').carrier = carrier

instance CompleteSublattice.instSetLike {α : Type u_1} [CompleteLattice α] : SetLike (CompleteSublattice α) α

instance CompleteSublattice.instPartialOrder {α : Type u_1} [CompleteLattice α] : PartialOrder (CompleteSublattice α)

theorem CompleteSublattice.top_mem {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : ⊤ ∈ L

theorem CompleteSublattice.bot_mem {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : ⊥ ∈ L

instance CompleteSublattice.instBot {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : Bot ↥L

instance CompleteSublattice.instTop {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : Top ↥L

instance CompleteSublattice.instSupSet {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : SupSet ↥L

instance CompleteSublattice.instInfSet {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : InfSet ↥L

theorem CompleteSublattice.sSupClosed {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {s : Set α} (h : s ⊆ ↑L) : sSup s ∈ L

theorem CompleteSublattice.sInfClosed {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {s : Set α} (h : s ⊆ ↑L) : sInf s ∈ L

@[simp]

theorem CompleteSublattice.coe_bot {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : ↑⊥ = ⊥

@[simp]

theorem CompleteSublattice.coe_top {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : ↑⊤ = ⊤

@[simp]

theorem CompleteSublattice.coe_sSup {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L) : ↑(sSup S) = sSup {x : α | ∃ s ∈ S, ↑s = x}

theorem CompleteSublattice.coe_sSup' {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L) : ↑(sSup S) = ⨆ N ∈ S, ↑N

@[simp]

theorem CompleteSublattice.coe_sInf {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L) : ↑(sInf S) = sInf {x : α | ∃ s ∈ S, ↑s = x}

theorem CompleteSublattice.coe_sInf' {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L) : ↑(sInf S) = ⨅ N ∈ S, ↑N

@[simp]

theorem CompleteSublattice.coe_iSup {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {ι : Sort u_3} (f : ι → ↥L) : ↑(iSup f) = ⨆ (i : ι), ↑(f i)

@[simp]

theorem CompleteSublattice.coe_iInf {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {ι : Sort u_3} (f : ι → ↥L) : ↑(iInf f) = ⨅ (i : ι), ↑(f i)

instance CompleteSublattice.instMaxSubtypeMem {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : Max ↥L

instance CompleteSublattice.instMinSubtypeMem {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : Min ↥L

instance CompleteSublattice.instCompleteLattice {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : CompleteLattice ↥L

def CompleteSublattice.subtype {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) : CompleteLatticeHom (↥L) α

The natural complete lattice hom from a complete sublattice to the original lattice.

@[simp]

theorem CompleteSublattice.coe_subtype {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) : ⇑L.subtype = Subtype.val

theorem CompleteSublattice.subtype_apply {α : Type u_1} [CompleteLattice α] (L : Sublattice α) (a : ↥L) : L.subtype a = ↑a

theorem CompleteSublattice.subtype_injective {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) : Function.Injective ⇑L.subtype

def CompleteSublattice.map {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice α) : CompleteSublattice β

The push forward of a complete sublattice under a complete lattice hom is a complete sublattice.

@[simp]

theorem CompleteSublattice.map_carrier {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice α) : (map f L).carrier = ⇑f '' ↑L

@[simp]

theorem CompleteSublattice.mem_map {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) {L : CompleteSublattice α} {b : β} : b ∈ map f L ↔ ∃ a ∈ L, f a = b

def CompleteSublattice.comap {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice β) : CompleteSublattice α

The pull back of a complete sublattice under a complete lattice hom is a complete sublattice.

@[simp]

theorem CompleteSublattice.comap_carrier {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice β) : (comap f L).carrier = ⇑f ⁻¹' ↑L

@[simp]

theorem CompleteSublattice.mem_comap {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) {L : CompleteSublattice β} {a : α} : a ∈ comap f L ↔ f a ∈ L

theorem CompleteSublattice.disjoint_iff {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L} : Disjoint a b ↔ Disjoint ↑a ↑b

theorem CompleteSublattice.codisjoint_iff {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L} : Codisjoint a b ↔ Codisjoint ↑a ↑b

theorem CompleteSublattice.isCompl_iff {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L} : IsCompl a b ↔ IsCompl ↑a ↑b

theorem CompleteSublattice.isComplemented_iff {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : ComplementedLattice ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b

instance CompleteSublattice.instTop_1 {α : Type u_1} [CompleteLattice α] : Top (CompleteSublattice α)

def CompleteSublattice.copy {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L) : CompleteSublattice α

Copy of a complete sublattice with a new carrier equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem CompleteSublattice.coe_copy {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L) : ↑(L.copy s hs) = s

theorem CompleteSublattice.copy_eq {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L) : L.copy s hs = L

def CompleteLatticeHom.range {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : CompleteSublattice β

The range of a CompleteLatticeHom is a CompleteSublattice.

See Note [range copy pattern].

theorem CompleteLatticeHom.range_coe {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : ↑f.range = Set.range ⇑f

noncomputable def CompleteLatticeHom.toOrderIsoRangeOfInjective {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (hf : Function.Injective ⇑f) : α ≃o ↥f.range

We can regard a complete lattice homomorphism as an order equivalence to its range.

@[simp]

theorem CompleteLatticeHom.toOrderIsoRangeOfInjective_apply {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (hf : Function.Injective ⇑f) (a : α) : (f.toOrderIsoRangeOfInjective hf) a = ⟨f a, ⋯⟩