English
An equivalence of group extensions can be constructed from a monoid hom f: E → E' that respects the inl inclusion and the rightHom projection; this yields an equivalence S.Equiv S'.
Русский
Из моноидной гомоморфии f: E → E', сохраняющей инъекции и правую проекцию, строится эквиваленция между расширениями групп.
LaTeX
$$$ \\text{ofMonoidHom}(f,comp\\_inl,rightHom\\_comp): S\\Equiv S' $$$
Lean4
/-- An equivalence of group extensions from a homomorphism making a commuting diagram. Such a
homomorphism is necessarily an isomorphism. -/
@[to_additive /-- An equivalence of additive group extensions from a homomorphism making a commuting diagram.
Such a homomorphism is necessarily an isomorphism. -/
]
noncomputable def ofMonoidHom (f : E →* E') (comp_inl : f.comp S.inl = S'.inl)
(rightHom_comp : S'.rightHom.comp f = S.rightHom) : S.Equiv S'
where
__ := f
invFun
e' :=
let e := Function.surjInv S.rightHom_surjective (S'.rightHom e')
e * S.inl (Function.invFun S'.inl ((f e)⁻¹ * e'))
left_inv
e := by
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, ← map_inv, ← map_mul]
obtain ⟨n, hn⟩ : (Function.surjInv S.rightHom_surjective (S'.rightHom (f e)))⁻¹ * e ∈ S.inl.range :=
by
rw [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ← MonoidHom.comp_apply, rightHom_comp]
simpa only [Function.surjInv_eq] using inv_mul_cancel (S.rightHom e)
rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl, Function.leftInverse_invFun S'.inl_injective]
right_inv
e' := by
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, map_mul]
rw [← eq_inv_mul_iff_mul_eq, ← MonoidHom.comp_apply, comp_inl]
apply Function.invFun_eq
rw [← MonoidHom.mem_range, S'.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ←
MonoidHom.comp_apply, rightHom_comp]
simpa only [Function.surjInv_eq] using inv_mul_cancel (S'.rightHom e')
inl_comm := congrArg DFunLike.coe comp_inl
rightHom_comm := congrArg DFunLike.coe rightHom_comp
