autMap_unique — Mathlib

English

If there is a commuting diagram f ≫ τ.hom = σ.hom ≫ f, then autMap f σ = τ.

Русский

Если диаграмма $f \\gg τ.hom = σ.hom \\gg f$ коммутирует, то autMap f σ = τ.

LaTeX

$$$\\text{autMap f }\\sigma = \\tau \\quad\\text{whenever}\\quad f\\gg\\tau.hom = \\sigma.hom\\gg f$$$

Lean4

/-- `autMap` is uniquely characterized by making the canonical diagram commute. -/
theorem autMap_unique {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A) (τ : Aut B)
    (h : f ≫ τ.hom = σ.hom ≫ f) : autMap f σ = τ :=
  ((exists_autMap f σ).choose_spec.right τ h).symm

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