Nyll.EtaleFundamentalGroups.Inertia.NormalizationComponentQuotient

theorem

galoisPullbackComponentQuotient_eq_of_equivariant

AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotient_eq_of_equivariant

Documentation

Equivariance identifies a given lift with its actual pointed-component quotient image. The only lifting input is the displayed equality of actual cover maps, which is supplied geometrically below.

Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups.Inertia
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y S : 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_eq_of_equivariant
    (tau : Aut Z) (sigma : Aut W)
    (htau : tau.hom ≫ i = i ≫ (pullback f).map sigma.hom) :
    galoisPullbackComponentQuotientMonoidHom
        f xi W hW w Z i z hiz hZ hi (MulOpposite.op tau) =
      MulOpposite.op sigma

theorem

galoisPullbackComponentQuotient_exists_normalized_fixed_lift

L71 ↗

AlgebraicGeometry.FiniteEtale.galoisPullbackComponentQuotient_exists_normalized_fixed_lift

Documentation

A normalized geometric-point stabilizer lifts to the component stabilizer, and its image under the actual canonical component quotient is the original deck transformation.

Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups.Inertia
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y S : 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 · full declaration

theorem galoisPullbackComponentQuotient_exists_normalized_fixed_lift
    (g : ((pullback f).obj W).left ⟶ S) [QuasiCompact g] [QuasiSeparated g]
    [IsIntegral Z.left]
    {Omega' : Type u} [Field Omega']
    (q : Spec (.of Omega') ⟶ (i.left ≫ g).normalization)
    (sigma : Aut W)
    (hsigma : ((pullback f).map sigma.hom).left ≫ g = g)
    (hfix : q ≫ normalizationComponentInclusion g i ≫
        normalizationEndomorphism g ((pullback f).map sigma.hom).left hsigma =
      q ≫ normalizationComponentInclusion g i) :
    ∃ (tau : Aut Z)
      (htau : tau.hom ≫ i = i ≫ (pullback f).map sigma.hom),
      galoisPullbackComponentQuotientMonoidHom
          f xi W hW w Z i z hiz hZ hi (MulOpposite.op tau) =
        MulOpposite.op sigma ∧
      q ≫ normalizationEndomorphism (i.left ≫ g) tau.hom.left (by
        have h := congrArg (fun k : Z ⟶ (pullback f).obj W => k.left) htau
        change tau.hom.left ≫ i.left =
          i.left ≫ ((pullback f).map sigma.hom).left at h
        rw [← Category.assoc, h, Category.assoc, hsigma]) = q := by
  let : Mono i := hi
  let : IsGalois Z := hZ
  obtain ⟨tau, htau, hfixed⟩ :=
    exists_aut_component_lift_of_fixes_normalized_geometricPoint
      g i q ((pullback f).mapIso sigma) hsigma hfix
  exact ⟨tau, htau,
    galoisPullbackComponentQuotient_eq_of_equivariant
      f xi W hW w Z i z hiz hZ hi tau sigma htau,
    hfixed⟩

NormalizationComponentQuotient.lean

Module documentation

Normalized component stabilizers and the canonical deck quotient

galoisPullbackComponentQuotient_eq_of_equivariant

galoisPullbackComponentQuotient_exists_normalized_fixed_lift

Module documentation

Normalized component stabilizers and the canonical deck quotient

Declarations

galoisPullbackComponentQuotient_eq_of_equivariant

galoisPullbackComponentQuotient_exists_normalized_fixed_lift