toAut_injective_of_non_trivial — Mathlib

English

toAut is injective if nontrivial elements act nontrivially on some fiber; i.e., if g ≠ 1 then there exists X,x with g • x ≠ x.

Русский

toAut инъективен, если не тривиален элемент действует не тривиально на каком-либо волокне; то есть существует X, x, такой что g • x ≠ x.

LaTeX

$$$\text{toAut is injective}$ under the stated nontriviality condition: $\forall g\neq 1, \exists X, x: g\cdot x \neq x$$$

Lean4

/-- `toAut` is injective, if only the identity acts trivially on every fiber. -/
theorem toAut_injective_of_non_trivial (h : ∀ (g : G), (∀ (X : C) (x : F.obj X), g • x = x) → g = 1) :
    Function.Injective (toAut F G) := by
  rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]
  intro g (hg : toAut F G g = 1)
  refine h g (fun X x ↦ ?_)
  have : (toAut F G g).hom.app X = 𝟙 (F.obj X) := by
    rw [hg]
    rfl
  rw [← toAut_hom_app_apply, this, FintypeCat.id_apply]

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