instIsFundamentalGroupAutFunctorFintypeCat

English

If a group element g acts trivially on every fiber, then g is the identity.

Русский

Если элемент группы g действует trivильно на каждом волокне, то g — единица.

LaTeX

$$$(\forall X)\ (\forall x\in F(X)),\; g\cdot x = x \Rightarrow g = 1$$$

Lean4

/-- `Aut F` is a fundamental group for `F`. -/
instance : IsFundamentalGroup F (Aut F)
    where
  naturality g _ _ f x := (FunctorToFintypeCat.naturality F F g.hom f x).symm
  transitive_of_isGalois X := FiberFunctor.isPretransitive_of_isConnected F X
  continuous_smul X := continuousSMul_aut_fiber F X
  non_trivial' g
    h := by
    ext X x
    exact h X x

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