English
The equivalence equiv is defined as a MulEquiv between G and Aut(forget k G) using the bijection equivHom k G and its injectivity/surjectivity.
Русский
Определение эквивалентности equiv как MulEquiv между G и Aut(forget k G) через биекцию equivHom k G и ее инъективность/сюрьективность.
LaTeX
$$def equiv [IsDomain k] : G ≃* Aut (forget k G) := MulEquiv.ofBijective (equivHom k G) ⟨equivHom_injective, equivHom_surjective⟩$$
Lean4
/-- Tannaka duality for finite groups:
A finite group `G` is isomorphic to `Aut (forget k G)`, where `k` is any integral domain,
and `forget k G` is the monoidal forgetful functor `FDRep k G ⥤ FGModuleCat k G`. -/
def equiv [IsDomain k] : G ≃* Aut (forget k G) :=
MulEquiv.ofBijective (equivHom k G) ⟨equivHom_injective, equivHom_surjective⟩
