toAut — Mathlib

English

If a group G acts naturally on F.obj X for each X, then there is a canonical homomorphism from G to Aut F.

Русский

Если G действует естественно на F.obj X для каждого X, существует канонический гомоморфизм из G в Aut F.

LaTeX

$$$\text{toAut}: G \to* Aut F$$$

Lean4

/-- If `G` acts naturally on `F.obj X` for each `X : C`, this is the canonical
group homomorphism into the automorphism group of `F`. -/
def toAut : G →* Aut F
    where
  toFun
    g :=
    NatIso.ofComponents (isoOnObj F g) <| by
      intro X Y f
      ext
      simp [IsNaturalSMul.naturality]
  map_one' := by
    ext
    simp only [NatIso.ofComponents_hom_app, isoOnObj_hom, one_smul]
    rfl
  map_mul' := by
    intro g h
    ext X x
    simp only [NatIso.ofComponents_hom_app, isoOnObj_hom, mul_smul]
    rfl

Похожие утверждения