Sublattices

This file defines sublattices.

TODO

Subsemilattices, if people care about them.

Tags

sublattice

structure Sublattice (α : Type u_2) [Lattice α] : Type u_2

A sublattice of a lattice is a set containing the suprema and infima of any of its elements.

• carrier : Set α

  The underlying set of a sublattice. Do not use directly. Instead, use the coercion Sublattice α → Set α, which Lean should automatically insert for you in most cases.

• supClosed' : SupClosed self.carrier
• infClosed' : InfClosed self.carrier

instance Sublattice.instSetLike {α : Type u_2} [Lattice α] : SetLike (Sublattice α) α

Equations

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

@[inline, reducible]

abbrev Sublattice.ofIsSublattice {α : Type u_2} [Lattice α] (s : Set α) (hs : IsSublattice s) : Sublattice α

Turn a set closed under supremum and infimum into a sublattice.

Equations

• Sublattice.ofIsSublattice s hs = { carrier := s, supClosed' := (_ : SupClosed s), infClosed' := (_ : InfClosed s) }

theorem Sublattice.coe_inj {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} : ↑L = ↑M ↔ L = M

@[simp]

theorem Sublattice.supClosed {α : Type u_2} [Lattice α] (L : Sublattice α) : SupClosed ↑L

@[simp]

theorem Sublattice.infClosed {α : Type u_2} [Lattice α] (L : Sublattice α) : InfClosed ↑L

@[simp]

theorem Sublattice.isSublattice {α : Type u_2} [Lattice α] (L : Sublattice α) : IsSublattice ↑L

@[simp]

theorem Sublattice.mem_carrier {α : Type u_2} [Lattice α] {L : Sublattice α} {a : α} : a ∈ L.carrier ↔ a ∈ L

@[simp]

theorem Sublattice.mem_mk {α : Type u_2} [Lattice α] {s : Set α} {a : α} (h_sup : SupClosed s) (h_inf : InfClosed s) : a ∈ { carrier := s, supClosed' := h_sup, infClosed' := h_inf } ↔ a ∈ s

@[simp]

theorem Sublattice.coe_mk {α : Type u_2} [Lattice α] {s : Set α} (h_sup : SupClosed s) (h_inf : InfClosed s) : ↑{ carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s

@[simp]

theorem Sublattice.mk_le_mk {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) : { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } ≤ { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔ s ⊆ t

@[simp]

theorem Sublattice.mk_lt_mk {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) : { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } < { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔ s ⊂ t

def Sublattice.copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : Sublattice α

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

Equations

• Sublattice.copy L s hs = { carrier := s, supClosed' := (_ : SupClosed s), infClosed' := (_ : InfClosed s) }

@[simp]

theorem Sublattice.coe_copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : ↑(Sublattice.copy L s hs) = s

theorem Sublattice.copy_eq {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = ↑L) : Sublattice.copy L s hs = L

theorem Sublattice.ext {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} : (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M

Two sublattices are equal if they have the same elements.

instance Sublattice.instSupCoe {α : Type u_2} [Lattice α] {L : Sublattice α} : Sup ↥L

A sublattice of a lattice inherits a supremum.

Equations

• Sublattice.instSupCoe = { sup := fun (a b : ↥L) => { val := ↑a ⊔ ↑b, property := (_ : ↑a ⊔ ↑b ∈ ↑L) } }

instance Sublattice.instInfCoe {α : Type u_2} [Lattice α] {L : Sublattice α} : Inf ↥L

A sublattice of a lattice inherits an infimum.

Equations

• Sublattice.instInfCoe = { inf := fun (a b : ↥L) => { val := ↑a ⊓ ↑b, property := (_ : ↑a ⊓ ↑b ∈ ↑L) } }

@[simp]

theorem Sublattice.coe_sup {α : Type u_2} [Lattice α] {L : Sublattice α} (a : ↥L) (b : ↥L) : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem Sublattice.coe_inf {α : Type u_2} [Lattice α] {L : Sublattice α} (a : ↥L) (b : ↥L) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem Sublattice.mk_sup_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a : α) (b : α) (ha : a ∈ L) (hb : b ∈ L) : { val := a, property := ha } ⊔ { val := b, property := hb } = { val := a ⊔ b, property := (_ : a ⊔ b ∈ ↑L) }

@[simp]

theorem Sublattice.mk_inf_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a : α) (b : α) (ha : a ∈ L) (hb : b ∈ L) : { val := a, property := ha } ⊓ { val := b, property := hb } = { val := a ⊓ b, property := (_ : a ⊓ b ∈ ↑L) }

instance Sublattice.instLatticeCoe {α : Type u_2} [Lattice α] (L : Sublattice α) : Lattice ↥L

A sublattice of a lattice inherits a lattice structure.

Equations

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

instance Sublattice.instDistribLatticeCoe {α : Type u_5} [DistribLattice α] (L : Sublattice α) : DistribLattice ↥L

A sublattice of a distributive lattice inherits a distributive lattice structure.

Equations

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

def Sublattice.subtype {α : Type u_2} [Lattice α] (L : Sublattice α) : LatticeHom (↥L) α

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

Equations

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

@[simp]

theorem Sublattice.coe_subtype {α : Type u_2} [Lattice α] (L : Sublattice α) : ⇑(Sublattice.subtype L) = Subtype.val

theorem Sublattice.subtype_apply {α : Type u_2} [Lattice α] (L : Sublattice α) (a : ↥L) : (Sublattice.subtype L) a = ↑a

theorem Sublattice.subtype_injective {α : Type u_2} [Lattice α] (L : Sublattice α) : Function.Injective ⇑(Sublattice.subtype L)

def Sublattice.inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L ≤ M) : LatticeHom ↥L ↥M

The inclusion homomorphism from a sublattice L to a bigger sublattice M.

Equations

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

@[simp]

theorem Sublattice.coe_inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L ≤ M) : ⇑(Sublattice.inclusion h) = Set.inclusion h

theorem Sublattice.inclusion_apply {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L ≤ M) (a : ↥L) : (Sublattice.inclusion h) a = Set.inclusion h a

theorem Sublattice.inclusion_injective {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L ≤ M) : Function.Injective ⇑(Sublattice.inclusion h)

@[simp]

theorem Sublattice.inclusion_rfl {α : Type u_2} [Lattice α] (L : Sublattice α) : Sublattice.inclusion (_ : L ≤ L) = LatticeHom.id ↥L

@[simp]

theorem Sublattice.subtype_comp_inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L ≤ M) : LatticeHom.comp (Sublattice.subtype M) (Sublattice.inclusion h) = Sublattice.subtype L

instance Sublattice.instTop {α : Type u_2} [Lattice α] : Top (Sublattice α)

The maximum sublattice of a lattice.

Equations

• Sublattice.instTop = { top := { carrier := Set.univ, supClosed' := (_ : SupClosed Set.univ), infClosed' := (_ : InfClosed Set.univ) } }

instance Sublattice.instBot {α : Type u_2} [Lattice α] : Bot (Sublattice α)

The empty sublattice of a lattice.

Equations

• Sublattice.instBot = { bot := { carrier := ∅, supClosed' := (_ : SupClosed ∅), infClosed' := (_ : InfClosed ∅) } }

instance Sublattice.instInf {α : Type u_2} [Lattice α] : Inf (Sublattice α)

The inf of two sublattices is their intersection.

Equations

• Sublattice.instInf = { inf := fun (L M : Sublattice α) => { carrier := ↑L ∩ ↑M, supClosed' := (_ : SupClosed (↑L ∩ ↑M)), infClosed' := (_ : InfClosed (↑L ∩ ↑M)) } }

instance Sublattice.instInfSet {α : Type u_2} [Lattice α] : InfSet (Sublattice α)

The inf of sublattices is their intersection.

Equations

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

instance Sublattice.instInhabited {α : Type u_2} [Lattice α] : Inhabited (Sublattice α)

Equations

• Sublattice.instInhabited = { default := ⊥ }

def Sublattice.topEquiv {α : Type u_2} [Lattice α] : ↥⊤ ≃o α

The top sublattice is isomorphic to the lattice.

This is the sublattice version of Equiv.Set.univ α.

Equations

• Sublattice.topEquiv = { toEquiv := Equiv.Set.univ α, map_rel_iff' := (_ : ∀ {a b : ↥⊤}, (Equiv.Set.univ α) a ≤ (Equiv.Set.univ α) b ↔ (Equiv.Set.univ α) a ≤ (Equiv.Set.univ α) b) }

@[simp]

theorem Sublattice.coe_top {α : Type u_2} [Lattice α] : ↑⊤ = Set.univ

@[simp]

theorem Sublattice.coe_bot {α : Type u_2} [Lattice α] : ↑⊥ = ∅

@[simp]

theorem Sublattice.coe_inf' {α : Type u_2} [Lattice α] (L : Sublattice α) (M : Sublattice α) : ↑(L ⊓ M) = ↑L ∩ ↑M

@[simp]

theorem Sublattice.coe_sInf {α : Type u_2} [Lattice α] (S : Set (Sublattice α)) : ↑(sInf S) = ⋂ L ∈ S, ↑L

@[simp]

theorem Sublattice.coe_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] (f : ι → Sublattice α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem Sublattice.coe_eq_univ {α : Type u_2} [Lattice α] {L : Sublattice α} : ↑L = Set.univ ↔ L = ⊤

@[simp]

theorem Sublattice.coe_eq_empty {α : Type u_2} [Lattice α] {L : Sublattice α} : ↑L = ∅ ↔ L = ⊥

@[simp]

theorem Sublattice.not_mem_bot {α : Type u_2} [Lattice α] (a : α) : a ∉ ⊥

@[simp]

theorem Sublattice.mem_top {α : Type u_2} [Lattice α] (a : α) : a ∈ ⊤

@[simp]

theorem Sublattice.mem_inf {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} {a : α} : a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M

@[simp]

theorem Sublattice.mem_sInf {α : Type u_2} [Lattice α] {a : α} {S : Set (Sublattice α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

@[simp]

theorem Sublattice.mem_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] {a : α} {f : ι → Sublattice α} : a ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

instance Sublattice.instCompleteLattice {α : Type u_2} [Lattice α] : CompleteLattice (Sublattice α)

Sublattices of a lattice form a complete lattice.

Equations

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

theorem Sublattice.subsingleton_iff {α : Type u_2} [Lattice α] : Subsingleton (Sublattice α) ↔ IsEmpty α

instance Sublattice.instUniqueSublattice {α : Type u_2} [Lattice α] [IsEmpty α] : Unique (Sublattice α)

Equations

• Sublattice.instUniqueSublattice = { toInhabited := Sublattice.instInhabited, uniq := (_ : ∀ (x : Sublattice α), x = default) }

def Sublattice.comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice β) : Sublattice α

The preimage of a sublattice along a lattice homomorphism.

Equations

• Sublattice.comap f L = { carrier := ⇑f ⁻¹' ↑L, supClosed' := (_ : SupClosed (⇑f ⁻¹' ↑L)), infClosed' := (_ : InfClosed (⇑f ⁻¹' ↑L)) }

@[simp]

theorem Sublattice.coe_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (f : LatticeHom α β) : ↑(Sublattice.comap f L) = ⇑f ⁻¹' ↑L

@[simp]

theorem Sublattice.mem_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} {a : α} {L : Sublattice β} : a ∈ Sublattice.comap f L ↔ f a ∈ L

theorem Sublattice.comap_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} : Monotone (Sublattice.comap f)

@[simp]

theorem Sublattice.comap_id {α : Type u_2} [Lattice α] (L : Sublattice α) : Sublattice.comap (LatticeHom.id α) L = L

@[simp]

theorem Sublattice.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] (L : Sublattice γ) (g : LatticeHom β γ) (f : LatticeHom α β) : Sublattice.comap f (Sublattice.comap g L) = Sublattice.comap (LatticeHom.comp g f) L

def Sublattice.map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : Sublattice β

The image of a sublattice along a monoid homomorphism is a sublattice.

Equations

• Sublattice.map f L = { carrier := ⇑f '' ↑L, supClosed' := (_ : SupClosed (⇑f '' ↑L)), infClosed' := (_ : InfClosed (⇑f '' ↑L)) }

@[simp]

theorem Sublattice.coe_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) : ↑(Sublattice.map f L) = ⇑f '' ↑L

@[simp]

theorem Sublattice.mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {b : β} : b ∈ Sublattice.map f L ↔ ∃ a ∈ L, f a = b

theorem Sublattice.mem_map_of_mem {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) {a : α} : a ∈ L → f a ∈ Sublattice.map f L

theorem Sublattice.apply_coe_mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) (a : ↥L) : f ↑a ∈ Sublattice.map f L

theorem Sublattice.map_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} : Monotone (Sublattice.map f)

@[simp]

theorem Sublattice.map_id {α : Type u_2} [Lattice α] {L : Sublattice α} : Sublattice.map (LatticeHom.id α) L = L

@[simp]

theorem Sublattice.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] {L : Sublattice α} (g : LatticeHom β γ) (f : LatticeHom α β) : Sublattice.map g (Sublattice.map f L) = Sublattice.map (LatticeHom.comp g f) L

theorem Sublattice.mem_map_equiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : α ≃o β} {a : β} : a ∈ Sublattice.map { toSupHom := { toFun := ⇑f, map_sup' := (_ : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) }, map_inf' := (_ : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) } L ↔ (OrderIso.symm f) a ∈ L

theorem Sublattice.apply_mem_map_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {a : α} (hf : Function.Injective ⇑f) : f a ∈ Sublattice.map f L ↔ a ∈ L

theorem Sublattice.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : α ≃o β) (L : Sublattice α) : Sublattice.map { toSupHom := { toFun := ⇑f, map_sup' := (_ : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) }, map_inf' := (_ : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) } L = Sublattice.comap { toSupHom := { toFun := ⇑(OrderIso.symm f), map_sup' := (_ : ∀ (a b : β), (OrderIso.symm f) (a ⊔ b) = (OrderIso.symm f) a ⊔ (OrderIso.symm f) b) }, map_inf' := (_ : ∀ (a b : β), (OrderIso.symm f) (a ⊓ b) = (OrderIso.symm f) a ⊓ (OrderIso.symm f) b) } L

theorem Sublattice.comap_equiv_eq_map_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : β ≃o α) (L : Sublattice α) : Sublattice.comap { toSupHom := { toFun := ⇑f, map_sup' := (_ : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) }, map_inf' := (_ : ∀ (a b : β), f (a ⊓ b) = f a ⊓ f b) } L = Sublattice.map { toSupHom := { toFun := ⇑(OrderIso.symm f), map_sup' := (_ : ∀ (a b : α), (OrderIso.symm f) (a ⊔ b) = (OrderIso.symm f) a ⊔ (OrderIso.symm f) b) }, map_inf' := (_ : ∀ (a b : α), (OrderIso.symm f) (a ⊓ b) = (OrderIso.symm f) a ⊓ (OrderIso.symm f) b) } L

theorem Sublattice.map_symm_eq_iff_eq_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {e : β ≃o α} : Sublattice.map { toSupHom := { toFun := ⇑(OrderIso.symm e), map_sup' := (_ : ∀ (a b : α), (OrderIso.symm e) (a ⊔ b) = (OrderIso.symm e) a ⊔ (OrderIso.symm e) b) }, map_inf' := (_ : ∀ (a b : α), (OrderIso.symm e) (a ⊓ b) = (OrderIso.symm e) a ⊓ (OrderIso.symm e) b) } L = M ↔ L = Sublattice.map { toSupHom := { toFun := ⇑e, map_sup' := (_ : ∀ (a b : β), e (a ⊔ b) = e a ⊔ e b) }, map_inf' := (_ : ∀ (a b : β), e (a ⊓ b) = e a ⊓ e b) } M

theorem Sublattice.map_le_iff_le_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {M : Sublattice β} : Sublattice.map f L ≤ M ↔ L ≤ Sublattice.comap f M

theorem Sublattice.gc_map_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : GaloisConnection (Sublattice.map f) (Sublattice.comap f)

@[simp]

theorem Sublattice.map_bot {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : Sublattice.map f ⊥ = ⊥

theorem Sublattice.map_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) (M : Sublattice α) : Sublattice.map f (L ⊔ M) = Sublattice.map f L ⊔ Sublattice.map f M

theorem Sublattice.map_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ι → Sublattice α) : Sublattice.map f (⨆ (i : ι), L i) = ⨆ (i : ι), Sublattice.map f (L i)

@[simp]

theorem Sublattice.comap_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : Sublattice.comap f ⊤ = ⊤

theorem Sublattice.comap_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (M : Sublattice β) (f : LatticeHom α β) : Sublattice.comap f (L ⊓ M) = Sublattice.comap f L ⊓ Sublattice.comap f M

theorem Sublattice.comap_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (s : ι → Sublattice β) : Sublattice.comap f (iInf s) = ⨅ (i : ι), Sublattice.comap f (s i)

theorem Sublattice.map_inf_le {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice α) (f : LatticeHom α β) : Sublattice.map f (L ⊓ M) ≤ Sublattice.map f L ⊓ Sublattice.map f M

theorem Sublattice.le_comap_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (M : Sublattice β) (f : LatticeHom α β) : Sublattice.comap f L ⊔ Sublattice.comap f M ≤ Sublattice.comap f (L ⊔ M)

theorem Sublattice.le_comap_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ι → Sublattice β) : ⨆ (i : ι), Sublattice.comap f (L i) ≤ Sublattice.comap f (⨆ (i : ι), L i)

theorem Sublattice.map_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice α) (f : LatticeHom α β) (hf : Function.Injective ⇑f) : Sublattice.map f (L ⊓ M) = Sublattice.map f L ⊓ Sublattice.map f M

theorem Sublattice.map_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (h : Function.Surjective ⇑f) : Sublattice.map f ⊤ = ⊤