Module

PullbackComponentStabilizer.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponentStabilizer

2 declarations indexed from sourceView source ↗

Module documentation

The deck group of a pullback component and its setwise stabilizer

The image of the canonical deck-group homomorphism for a pointed Galois pullback component consists exactly of the original deck transformations preserving the component's geometric-fiber range. In fact, it suffices that the distinguished point is mapped back into that range: transitivity of the component deck group constructs a lift, and evaluation on the original connected cover proves that its image is the prescribed transformation.

This is a statement about actual cover automorphisms and their fiber actions. No lifting or equivariance assumption is introduced. To use it for inertia on a normalization, one must still prove geometrically that fixing the chosen normalization point preserves the relevant component.

Imports2

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponentEquivariance
Mathlib.CategoryTheory.Galois.GaloisObjects

Imported by2

theorem

galoisPullbackComponentQuotient_exists_lift_of_mem_range

L51 ↗

AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotient_exists_lift_of_mem_range

Documentation

An original deck transformation lifts to the chosen Galois component as soon as it maps the distinguished fiber point back into that component. The lift is constructed using the transitive component deck action.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
variable (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
  (W : FiniteEtale Y) (hW : IsGalois W)
  (w : (fiber (xi ≫ f)).obj W)
  (Z : FiniteEtale X) (i : Z ⟶ (pullback f).obj W)
  (z : (fiber xi).obj Z)
  (hiz : (fiber xi).map i z =
    transportedPointOfCompIso (pullback f) (pullbackFiberIso f xi) W w)
  (hZ : IsGalois Z) (hi : Mono i)

Lean source · statement

theorem galoisPullbackComponentQuotient_exists_lift_of_mem_range
    (sigma : (Aut W)ᵐᵒᵖ)
    (hsigma : (fiber xi).map ((pullback f).map sigma.unop.hom)
      ((fiber xi).map i z) ∈ Set.range ((fiber xi).map i)) :
    ∃ tau : (Aut Z)ᵐᵒᵖ,
      galoisPullbackComponentQuotientMonoidHom
          f xi W hW w Z i z hiz hZ hi tau = sigma ∧
        tau.unop.hom ≫ i = i ≫ (pullback f).map sigma.unop.hom

theorem

galoisPullbackComponentQuotientMonoidHom_mem_range_iff_preserves_component

L105 ↗

AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_mem_range_iff_preserves_component