English
For a multiplicative equivalence f : M ≃* N and a relation rel on N, the pullback along f of map_mul together with conGen rel equals the conGen of the pullback relation: Con.comap f (map_mul f) (conGen rel) = conGen (λ x y, rel (f x) (f y)).
Русский
При биекции по умножению f: M ≃* N и отношении rel на N сопоставление вытягивания конгруэнции вдоль f с конгруэнцией конгенера rel равны: Con.comap f (map_mul f) (conGen rel) = conGen (λ x y, rel (f x) (f y)).
LaTeX
$$Con.comap f (map_mul f) (conGen rel) = conGen (fun x y ↦ rel (f x) (f y))$$
Lean4
@[to_additive]
theorem comap_conGen_equiv {M N : Type*} [Mul M] [Mul N] (f : MulEquiv M N) (rel : N → N → Prop) :
Con.comap f (map_mul f) (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) :=
by
apply le_antisymm _ (le_comap_conGen f (map_mul f) rel)
intro a b h
simp only [Con.comap_rel] at h
have H : ∀ n1 n2, (conGen rel) n1 n2 → ∀ a b, f a = n1 → f b = n2 → (conGen fun x y ↦ rel (f x) (f y)) a b :=
by
intro n1 n2 h
induction h with
| of x y h =>
intro _ _ fa fb
apply ConGen.Rel.of
rwa [fa, fb]
| refl x =>
intro _ _ fc fd
rw [f.injective (fc.trans fd.symm)]
exact ConGen.Rel.refl _
| symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
| trans _ _ ih ih1 =>
exact fun a b fa fb ↦
Exists.casesOn (f.surjective _) fun c' hc' ↦ ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
| mul _ _ ih ih1 =>
rename_i w x y z _ _
intro a b fa fb
rw [← f.eq_symm_apply, map_mul] at fa fb
rw [fa, fb]
exact
ConGen.Rel.mul (ih (f.symm w) (f.symm x) (by simp) (by simp)) (ih1 (f.symm y) (f.symm z) (by simp) (by simp))
exact H (f a) (f b) h a b (refl _) (refl _)
