AlgebraicGeometry.FiniteEtale.pointedFundamentalGroupHom_range_eq_stabilizer
The image of the pointed covering homomorphism is precisely the actual stabilizer of the geometric point of the covering fibre.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} [ConnectedSpace S]
{K : Type u} [Field K] [IsSepClosed K]Lean source · statement
theorem pointedFundamentalGroupHom_range_eq_stabilizer
(W : FiniteEtale S) (x : Spec (.of K) ⟶ W.left)
(y : Spec (.of K) ⟶ S) (hxy : x ≫ W.hom = y) :
(pointedFundamentalGroupHom W.hom x y hxy).toMonoidHom.range =
MulAction.stabilizer π₁ᵉᵗ(y)
((fiberObjEquivHom y W).symm (Over.homMk x hxy))