English
The kernel of a lattice homomorphism f is a lattice congruence on the domain: its relation identifies elements that map to the same image, and the induced infimum and supremum operations respect this relation.
Русский
Ядро гомоморфизма решётки f образует конгруэнцию на области определения: элементы, имеющие одинаковое образное значение, эквивалентны; операции meet и join сохраняют эту эквиваленцию.
LaTeX
$$$\\ker f \\text{ is a lattice congruence on } \\alpha$; the relation is given by equality of images, and the induced INF/SUP respect it.$$
Lean4
/-- The kernel of a lattice homomorphism as a lattice congruence. -/
@[simps!]
def ker [Lattice α] [Lattice β] [LatticeHomClass F α β] (f : F) : LatticeCon α
where
toSetoid := Setoid.ker f
inf _ _ := by simp_all only [Setoid.ker, onFun, map_inf]
sup _ _ := by simp_all only [Setoid.ker, onFun, map_sup]
