English
If T is order-generating, the pair (kernel, hull) induces a Galois insertion between the lattice of subsets of T and α^op, i.e., a dual adjoint relationship between kernel and hull.
Русский
Если T порождает порядок, пара (kernel, hull) задаёт голасову вставку между мультидуплексами подмножеств T и α^op.
LaTeX
$$$\\text{gi}(hG) : GaloisInsertion( α := Set\\ T, β := α^{\\mathrm{op}})\\Big(\\mathrm{OrderDual}^{-1} \\circ \\ker\\Big)\\Big(\\mathrm{hull}(T) \\circ \\mathrm{OrderDual}^{-1} \\Big).$$$
Lean4
/-- When `T` is order generating, the `kernel` and the `hull` form a Galois insertion
-/
def gi (hG : OrderGenerates T) :
GaloisInsertion (α := Set T) (β := αᵒᵈ) (OrderDual.toDual ∘ kernel) (hull T ∘ OrderDual.ofDual) :=
gc.toGaloisInsertion fun a ↦ by
obtain ⟨S, rfl⟩ := hG a
rw [OrderDual.le_toDual, kernel, kernel]
exact
sInf_le_sInf <|
image_val_mono fun c hcS => by
rw [hull, mem_preimage, mem_Ici]
exact CompleteSemilatticeInf.sInf_le _ _ (mem_image_of_mem Subtype.val hcS)
