autMap_apply_mul — Mathlib

English

There is a MonoidHom Aut A → Aut B given by autMap f, i.e., an algebraic morphism between Aut groups compatible with autMap.

Русский

Существует моноид-гомоморфизм Aut A → Aut B, названный autMap f, совместимый с autMap.

LaTeX

$$$\text{autMapHom } f : Aut A \to Aut B$ is a MonoidHom with $\text{map} = autMap f$ and compatibility.$$

Lean4

@[simp]
theorem autMap_apply_mul {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ τ : Aut A) :
    autMap f (σ * τ) = autMap f σ * autMap f τ :=
  by
  let F := GaloisCategory.getFiberFunctor C
  obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
  apply evaluation_aut_injective_of_isConnected F (B : C) (F.map f a)
  simp [Aut.Aut_mul_def]

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