comp_autMap_apply — Mathlib

English

For a morphism f : A ⟶ B with A connected and B Galois, and σ ∈ Aut A, there exists a unique τ ∈ Aut B such that f ≫ τ.hom = σ.hom ≫ f.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comp_autMap_apply (F : C ⥤ FintypeCat.{w}) {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ : Aut A)
    (a : F.obj A) : F.map (autMap f σ).hom (F.map f a) = F.map f (F.map σ.hom a) := by
  simpa [-comp_autMap] using congrFun (F.congr_map (comp_autMap f σ)) a

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