gi — Mathlib · SciLib

English

There exists a complete lattice structure on Subalgebra R A obtained via the lifted Galois insertion with gi.

Русский

Существет полная решетка на Subalgebra R A полученная через подъём Галиа-инсерции с gi.

LaTeX

$$$\text{CompleteLattice}(\mathrm{Subalgebra}\; R\; A)$$$

Lean4

/-- Galois insertion between `adjoin` and `coe`. -/
protected def gi : GaloisInsertion (adjoin R : Set A → Subalgebra R A) (↑)
    where
  choice s hs := (adjoin R s).copy s <| le_antisymm (Algebra.gc.le_u_l s) hs
  gc := Algebra.gc
  le_l_u S := (Algebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
  choice_eq _ _ := Subalgebra.copy_eq _ _ _

Похожие утверждения