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

@[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) : (CompleteSublattice.mk' carrier sSupClosed' sInfClosed').toSublattice.carrier = 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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CompleteSublattice.instBot = { bot := { val := ⊥, property := (_ : ⊥ ∈ L.toSublattice) } }

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

Equations

• CompleteSublattice.instTop = { top := { val := ⊤, property := (_ : ⊤ ∈ L.toSublattice) } }

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

Equations

• CompleteSublattice.instSupSet = { sSup := fun (s : Set ↥L) => { val := sSup (Subtype.val '' s), property := (_ : sSup (Subtype.val '' s) ∈ L.carrier) } }

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

Equations

• CompleteSublattice.instInfSet = { sInf := fun (s : Set ↥L) => { val := sInf (Subtype.val '' s), property := (_ : sInf (Subtype.val '' s) ∈ L.carrier) } }

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

theorem CompleteSublattice.isCompl_iff {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} {a : ↥L} {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.instTopCompleteSublattice {α : Type u_1} [CompleteLattice α] : Top (CompleteSublattice α)

Equations

• CompleteSublattice.instTopCompleteSublattice = { top := CompleteSublattice.mk' Set.univ (_ : ∀ x ⊆ Set.univ, sSup x ∈ Set.univ) (_ : ∀ x ⊆ Set.univ, sInf x ∈ Set.univ) }

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.

Equations

• CompleteSublattice.copy L s hs = CompleteSublattice.mk' s (_ : ∀ ⦃s_1 : Set α⦄, s_1 ⊆ s → sSup s_1 ∈ s) (_ : ∀ ⦃s_1 : Set α⦄, s_1 ⊆ s → sInf s_1 ∈ s)

@[simp]

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

theorem CompleteSublattice.copy_eq {α : Type u_1} [CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L) : CompleteSublattice.copy L 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].

Equations

• CompleteLatticeHom.range f = CompleteSublattice.copy (CompleteSublattice.map f ⊤) (Set.range ⇑f) (_ : Set.range ⇑f = ⇑f '' Set.univ)

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

@[simp]

theorem CompleteLatticeHom.toOrderIsoRangeOfInjective_apply {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (hf : Function.Injective ⇑f) (a : α) : (CompleteLatticeHom.toOrderIsoRangeOfInjective f hf) a = { val := f a, property := (_ : ∃ (y : α), (orderEmbeddingOfInjective f hf) y = (orderEmbeddingOfInjective f hf) a) }

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

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

Equations

• CompleteLatticeHom.toOrderIsoRangeOfInjective f hf = OrderEmbedding.orderIso