action_ext_of_isGalois — Mathlib

English

If an automorphism t of F matches the G-action on a single element x in F(X) for a Galois object X, then it matches on every element of F(X).

Русский

Если для точечного Galois-объекта X и элемента x в F(X) существует g такой, что g действует как t_X на x, то g действует так же на все элементы F(X).

LaTeX

$$$\forall X\,[IsGalois(X) ]\Rightarrow \forall g\in G,\forall x\in F(X),\; g\cdot x = t_X(x) \Rightarrow \forall y\in F(X),\; g\cdot y = t_X(y)$$$

Lean4

theorem action_ext_of_isGalois {t : F ⟶ F} {X : C} [IsGalois X] {g : G} (x : F.obj X) (hg : g • x = t.app X x)
    (y : F.obj X) : g • y = t.app X y :=
  by
  obtain ⟨φ, (rfl : F.map φ.hom y = x)⟩ := MulAction.exists_smul_eq (Aut X) y x
  have : Function.Injective (F.map φ.hom) := ConcreteCategory.injective_of_mono_of_preservesPullback (F.map φ.hom)
  apply this
  rw [IsNaturalSMul.naturality, hg, FunctorToFintypeCat.naturality]

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