autMap — Mathlib

English

For connected A and IsGalois B, given f : A ⟶ B and σ ∈ Aut A, there is a unique τ ∈ Aut B with f ≫ τ.hom = σ.hom ≫ f, and autMap f σ = τ.

Русский

Для связанного A и галуа B: при наличии f: A ⟶ B и σ ∈ Aut A существует уникальный τ ∈ Aut B такой, что f ≫ τ.hom = σ.hom ≫ f, и autMap f σ = τ.

LaTeX

$$$\exists!\tau:\ Aut B,\; f\!\gg\tau.hom = \sigma.hom\gg f$$$

Lean4

/-- A morphism from a connected object to a Galois object induces a map on automorphism
groups. This is a group homomorphism (see `autMapHom`). -/
noncomputable def autMap {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) : Aut B :=
  (exists_autMap f σ).choose

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