Module

PullbackComponent.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponent

2 declarations indexed from sourceView source ↗

Module documentation

Galois components of pulled-back covers

Pullback of a connected Galois cover need not remain connected. Nevertheless, the connected component containing the pullback of a chosen geometric-fiber point is again Galois. This is the componentwise form that is valid for an arbitrary morphism of connected base schemes.

Imports4

Imported by6

theorem

isGalois_of_stabilizer_normal

L33 ↗

AlgebraicGeometry.FiniteEtale.isGalois_of_stabilizer_normal

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u u₁ u₂ w
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem isGalois_of_stabilizer_normal
    {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (A : C) [IsConnected A] (a : F.obj A)
    (ha : (MulAction.stabilizer (Aut F) a).Normal) :
    IsGalois A

theorem

exists_galoisComponent_pullback

L99 ↗

AlgebraicGeometry.FiniteEtale.exists_galoisComponent_pullback

Documentation

A chosen geometric-fiber point of a pulled-back Galois cover lies in a connected component which is itself a Galois cover.