autMap_comp — Mathlib

English

For connected X and IsGalois Y, and morphisms f : X ⟶ Y and g : Y ⟶ Z, autMap(f ≫ g) = autMap g ∘ autMap f.

Русский

Для связанных X и галуа Y и морфизмов f: X ⟶ Y, g: Y ⟶ Z имеем autMap(f ≫ g) = autMap g ∘ autMap f.

LaTeX

$$$\operatorname{autMap}(f \circ g) = (\operatorname{autMap} g) \circ (\operatorname{autMap} f)$$$

Lean4

@[simp]
theorem autMap_comp {X Y Z : C} [IsConnected X] [IsGalois Y] [IsGalois Z] (f : X ⟶ Y) (g : Y ⟶ Z) :
    autMap (f ≫ g) = autMap g ∘ autMap f :=
  by
  refine funext fun σ ↦ autMap_unique _ σ _ ?_
  rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]
  simp

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