Module

PullbackComponentEquivariance.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponentEquivariance

1 declaration indexed from sourceView source ↗

Module documentation

Equivariance of the actual inclusion of a Galois pullback component

The homomorphism from the deck group of a pointed pullback component to the original deck group is defined using the two pointed fundamental-group quotients. This file proves that it intertwines the actual component inclusion with the pulled-back deck transformations. The compatibility is derived from surjectivity of the component quotient, naturality of the fiber comparison, and injectivity of evaluation on morphisms out of a connected cover.

This supplies the deck-equivariance input for subsequent comparisons of normalization geometric-point stabilizers. It does not identify those stabilizers with mapped local ideal inertia: choosing and comparing the normalization points is a separate geometric step.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCovers.PullbackComponentQuotient

Imported by4

theorem

galoisPullbackComponentQuotientMonoidHom_equivariant

L42 ↗

AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotientMonoidHom_equivariant

Documentation

The actual inclusion of a pointed Galois pullback component intertwines its deck transformations with the corresponding pulled-back original deck transformations. No equivariance hypothesis is added.

Source context 8 commands

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

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

Lean source · statement

theorem galoisPullbackComponentQuotientMonoidHom_equivariant
    (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)
    (sigma : (Aut Z)ᵐᵒᵖ) :
    sigma.unop.hom ≫ i =
      i ≫ (pullback f).map
        ((galoisPullbackComponentQuotientMonoidHom
          f xi W hW w Z i z hiz hZ hi sigma).unop.hom)

Module documentation

Equivariance of the actual inclusion of a Galois pullback component

Declarations

galoisPullbackComponentQuotientMonoidHom_equivariant