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.

Equations

• CompleteSublattice.mk' carrier sSupClosed' sInfClosed' = { carrier := carrier, supClosed' := ⋯, infClosed' := ⋯, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' }

@[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').carrier = carrier

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

Equations

• CompleteSublattice.instSetLike = { coe := fun (L : CompleteSublattice α) => L.carrier, coe_injective' := ⋯ }

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

Equations

• CompleteSublattice.instBot = { bot := ⟨⊥, ⋯⟩ }

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

Equations

• CompleteSublattice.instTop = { top := ⟨⊤, ⋯⟩ }

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

Equations

• CompleteSublattice.instSupSet = { sSup := fun (s : Set ↥L) => ⟨sSup (Subtype.val '' s), ⋯⟩ }

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

Equations

• CompleteSublattice.instInfSet = { sInf := fun (s : Set ↥L) => ⟨sInf (Subtype.val '' s), ⋯⟩ }

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.instMaxSubtypeMem {α : Type u_1} [CompleteLattice α] {L : CompleteSublattice α} : Max ↥L

Equations

• CompleteSublattice.instMaxSubtypeMem = Sublattice.instSupCoe

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

Equations

• CompleteSublattice.instMinSubtypeMem = Sublattice.instInfCoe

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

Equations

• CompleteSublattice.instCompleteLattice = Function.Injective.completeLattice (fun (a : ↥L) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

Equations

• L.subtype = { toFun := Subtype.val, map_sInf' := ⋯, map_sSup' := ⋯ }

@[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.

Equations

• CompleteSublattice.map f L = { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯, sSupClosed' := ⋯, sInfClosed' := ⋯ }

@[simp]

theorem CompleteSublattice.map_carrier {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice α) : (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 ∈ CompleteSublattice.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.

Equations

• CompleteSublattice.comap f L = { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯, sSupClosed' := ⋯, sInfClosed' := ⋯ }

@[simp]

theorem CompleteSublattice.comap_carrier {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice β) : (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 ∈ CompleteSublattice.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 α)

Equations

• CompleteSublattice.instTop_1 = { top := CompleteSublattice.mk' 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

• L.copy s hs = CompleteSublattice.mk' s ⋯ ⋯

@[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].

Equations

• f.range = (CompleteSublattice.map f ⊤).copy (Set.range ⇑f) ⋯

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.

Equations

• f.toOrderIsoRangeOfInjective hf = OrderEmbedding.orderIso

@[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, ⋯⟩