English
Let f : M → N be a homomorphism and rel a relation on N. Then the generated congruence on M obtained by pulling back rel along f is contained in (and under suitable conditions equal to) the comap of the congruence generated by rel along f.
Русский
Пусть f : M → N — гомоморфизм и rel — отношение на N. Тогда порождаемая конгруэнция на M, полученная путем вытягивания rel обратно по f, содержится в конскомобразном (pullback) отношении along f и при некоторых условиях равна конгруенции, порождаемой rel на N.
LaTeX
$$conGen (x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel)$$
Lean4
@[to_additive]
theorem le_comap_conGen {M N : Type*} [Mul M] [Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y)
(rel : N → N → Prop) : conGen (fun x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel) :=
by
intro x y h
simp only [Con.comap_rel]
exact
.rec (fun x y h ↦ .of (f x) (f y) h) (fun x ↦ .refl (f x)) (fun _ h ↦ .symm h) (fun _ _ h1 h2 ↦ h1.trans h2)
(fun {w x y z} _ _ h1 h2 ↦
(congrArg (fun a ↦ conGen rel a (f (x * z))) (H w y)).mpr
(((congrArg (fun a ↦ conGen rel (f w * f y) a) (H x z))).mpr (.mul h1 h2)))
h
