Module

AbsoluteDivisorialFiniteQuotientCompatibility.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteDivisorialFiniteQuotientCompatibility

19 declarations indexed from sourceView source ↗

Module documentation

Absolute generic inertia and finite function-field quotients

An automorphism of a fixed separable closure of the function field maps to the fundamental group at the generic geometric point. This file compares its image on every pointed connected finite Galois cover with restriction to the cover's function field, using the embedding selected by the fiber point.

Imports5

Imported by2

theorem

fieldGeometricPoint_comp_genericExtensionMorphism

L32 ↗

EtaleFundamentalGroups.Inertia.fieldGeometricPoint_comp_genericExtensionMorphism

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem fieldGeometricPoint_comp_genericExtensionMorphism
    (U : Scheme.{u}) [IsIntegral U]
    (Omega : Type u) [Field Omega] [Algebra U.functionField Omega] :
    ξ U.functionField Omega ≫
        U.genericExtensionMorphism U.functionField =
      U.genericExtensionMorphism Omega

def

absoluteGenericFiberIso

L45 ↗

EtaleFundamentalGroups.Inertia.absoluteGenericFiberIso

Documentation

The canonical identification between the fiber at the composite generic geometric point and the fiber at the directly constructed generic geometric point.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def absoluteGenericFiberIso
    (U : Scheme.{u}) [IsIntegral U]
    (Omega : Type u) [Field Omega] [Algebra U.functionField Omega] :
    fiber (ξ U.functionField Omega ≫
        U.genericExtensionMorphism U.functionField) ≅
      fiber (U.genericExtensionMorphism Omega)

def

absoluteGenericGaloisToFundamentalGroup

L56 ↗

EtaleFundamentalGroups.Inertia.absoluteGenericGaloisToFundamentalGroup

Documentation

The homomorphism from the absolute Galois group of the function field to the fundamental group at its generic geometric point.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def absoluteGenericGaloisToFundamentalGroup
    (U : Scheme.{u}) [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega] :
    Gal(Omega/U.functionField) →*
      π₁ᵉᵗ(U.genericExtensionMorphism Omega)

theorem

absoluteGenericGaloisToFundamentalGroup_apply

L71 ↗

EtaleFundamentalGroups.Inertia.absoluteGenericGaloisToFundamentalGroup_apply

Documentation

Evaluation of the absolute generic Galois map as a conjugated fundamental-group automorphism.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem absoluteGenericGaloisToFundamentalGroup_apply
    {U : Scheme.{u}} [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    (sigma : Gal(Omega/U.functionField)) :
    absoluteGenericGaloisToFundamentalGroup U Omega sigma =
      (absoluteGenericFiberIso U Omega).conjAut
    (fundamentalGroupHom
      (U.genericExtensionMorphism U.functionField)
      (ξ U.functionField Omega)
      (absoluteGaloisToFiberAutMulEquiv U.functionField Omega
        (IsSepClosure.sep_closed U.functionField) sigma))

theorem

finiteEtaleGaloisCoverQuotient_absoluteGenericGalois_transport

L88 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleGaloisCoverQuotient_absoluteGenericGalois_transport

Documentation

The pointed quotient of an absolute generic Galois element is the corresponding quotient before transport from the composite generic point. This isolates the remaining comparison from generic lifts to function-field restriction.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem finiteEtaleGaloisCoverQuotient_absoluteGenericGalois_transport
    {U : Scheme.{u}} [IsIntegral U] [ConnectedSpace U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    [IsSepClosed Omega]
    (W : FiniteEtale U) (hW : IsGalois W)
    (w : (fiber (U.genericExtensionMorphism Omega)).obj W)
    (sigma : Gal(Omega/U.functionField)) :
    finiteEtaleGaloisCoverQuotientMonoidHom
        (U.genericExtensionMorphism Omega) W hW w
        (absoluteGenericGaloisToFundamentalGroup U Omega sigma) =
      finiteEtaleGaloisCoverQuotientMonoidHom
        (ξ U.functionField Omega ≫
          U.genericExtensionMorphism U.functionField)
        W hW ((absoluteGenericFiberIso U Omega).inv.app W w)
        (fundamentalGroupHom
          (U.genericExtensionMorphism U.functionField)
          (ξ U.functionField Omega)
          (absoluteGaloisToFiberAutMulEquiv U.functionField Omega
            (IsSepClosure.sep_closed U.functionField) sigma))

def

finiteEtaleFiberPointFunctionFieldAlgHom

L122 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleFiberPointFunctionFieldAlgHom

Documentation

A point of the generic geometric fiber selects the corresponding embedding of the function field of a connected finite-etale cover.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

def finiteEtaleFiberPointFunctionFieldAlgHom
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    [IsSepClosed Omega]
    (W : FiniteEtale U) [IsConnected W]
    (w : (fiber (U.genericExtensionMorphism Omega)).obj W) :
    letI : IsIntegral W.left :=
      isIntegral_left_of_isConnected_finiteEtale W
    letI : Algebra U.functionField W.left.functionField :=
      finiteEtaleFunctionFieldAlgebra W
    W.left.functionField →ₐ[U.functionField] Omega := by
  letI : IsIntegral W.left :=
    isIntegral_left_of_isConnected_finiteEtale W
  letI : Algebra U.functionField W.left.functionField :=
    finiteEtaleFunctionFieldAlgebra W
  exact finiteEtaleGenericHomFunctionFieldAlgHom W
    (fiberObjEquivHom (U.genericExtensionMorphism Omega) W w)

def

finiteEtaleFiberPointFunctionFieldAlgebra

L144 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleFiberPointFunctionFieldAlgebra

Documentation

The algebra structure on the geometric-point field selected by a point of a connected finite-etale cover. It is kept explicit because different fiber points generally select different embeddings.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

def finiteEtaleFiberPointFunctionFieldAlgebra
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    [IsSepClosed Omega]
    (W : FiniteEtale U) [IsConnected W]
    (w : (fiber (U.genericExtensionMorphism Omega)).obj W) :
    letI : IsIntegral W.left :=
      isIntegral_left_of_isConnected_finiteEtale W
    letI : Algebra U.functionField W.left.functionField :=
      finiteEtaleFunctionFieldAlgebra W
    Algebra W.left.functionField Omega := by
  letI : IsIntegral W.left :=
    isIntegral_left_of_isConnected_finiteEtale W
  letI : Algebra U.functionField W.left.functionField :=
    finiteEtaleFunctionFieldAlgebra W
  exact (finiteEtaleFiberPointFunctionFieldAlgHom W w).toRingHom.toAlgebra

theorem

finiteEtaleFiberPointFunctionFieldIsScalarTower

L164 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleFiberPointFunctionFieldIsScalarTower

Documentation

The point-selected function-field embedding extends the fixed embedding of the base function field.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem finiteEtaleFiberPointFunctionFieldIsScalarTower
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    [IsSepClosed Omega]
    (W : FiniteEtale U) [IsConnected W]
    (w : (fiber (U.genericExtensionMorphism Omega)).obj W) :
    letI : IsIntegral W.left :=
      isIntegral_left_of_isConnected_finiteEtale W
    letI : Algebra U.functionField W.left.functionField :=
      finiteEtaleFunctionFieldAlgebra W
    letI : Algebra W.left.functionField Omega :=
      finiteEtaleFiberPointFunctionFieldAlgebra W w
    IsScalarTower U.functionField W.left.functionField Omega := by
  let : IsIntegral W.left :=
    isIntegral_left_of_isConnected_finiteEtale W
  let : Algebra U.functionField W.left.functionField :=
    finiteEtaleFunctionFieldAlgebra W
  let j := finiteEtaleFiberPointFunctionFieldAlgHom W w
  let : Algebra W.left.functionField Omega :=
    finiteEtaleFiberPointFunctionFieldAlgebra W w
  apply IsScalarTower.of_algebraMap_eq'
  ext z
  exact (j.commutes z).symm

def

genericPointLiftPrecomp

L191 ↗

EtaleFundamentalGroups.Inertia.genericPointLiftPrecomp

Documentation

Precompose a lift of the generic geometric point by an absolute Galois automorphism, retaining it as a morphism over the base scheme.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def genericPointLiftPrecomp
    {U : Scheme.{u}} [IsIntegral U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U)
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma)
    (sigma : Gal(Omega/U.functionField)) :
    Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma

def

genericPointLiftSchemeHom

L225 ↗

EtaleFundamentalGroups.Inertia.genericPointLiftSchemeHom

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def genericPointLiftSchemeHom
    {U : Scheme.{u}} [IsIntegral U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U)
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma) :
    Spec (.of Omega) ⟶ W.left

theorem

genericPointLiftSchemeHom_comp

L233 ↗

EtaleFundamentalGroups.Inertia.genericPointLiftSchemeHom_comp

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem genericPointLiftSchemeHom_comp
    {U : Scheme.{u}} [IsIntegral U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U)
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma) :
    genericPointLiftSchemeHom W g ≫ W.hom =
      U.genericExtensionMorphism Omega

theorem

genericPointLiftSchemeHom_genericPoint

L260 ↗

EtaleFundamentalGroups.Inertia.genericPointLiftSchemeHom_genericPoint

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem genericPointLiftSchemeHom_genericPoint
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U) [IsConnected W]
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma) :
    letI : IsIntegral W.left :=
      isIntegral_left_of_isConnected_finiteEtale W
    genericPointLiftSchemeHom W g (IsLocalRing.closedPoint Omega) =
      genericPoint W.left := by
  let : IsIntegral W.left :=
    isIntegral_left_of_isConnected_finiteEtale W
  let f : W.left ⟶ U := W.hom
  let : IsFiniteEtale f := W.2
  have hg :
      f (genericPointLiftSchemeHom W g (IsLocalRing.closedPoint Omega)) =
        genericPoint U := by
    change (genericPointLiftSchemeHom W g ≫ W.hom)
        (IsLocalRing.closedPoint Omega) = genericPoint U
    exact (congrArg
      (fun r : Spec (.of Omega) ⟶ U ↦
        r (IsLocalRing.closedPoint Omega))
      (genericPointLiftSchemeHom_comp W g)).trans
        (U.genericExtensionMorphism_apply_closedPoint Omega)
  have hgeneric : f (genericPoint W.left) = genericPoint U :=
    f.map_genericPoint_of_denseRange
      (finiteEtale_hom_denseRange_of_isConnected W)
  symm
  apply (f.isDiscrete_preimage_singleton (genericPoint U)).eq_of_specializes
    (genericPoint_specializes
      (genericPointLiftSchemeHom W g (IsLocalRing.closedPoint Omega)))
  · exact hgeneric
  · exact hg

theorem

genericPointLiftSchemeHom_precomp

L294 ↗

EtaleFundamentalGroups.Inertia.genericPointLiftSchemeHom_precomp

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem genericPointLiftSchemeHom_precomp
    {U : Scheme.{u}} [IsIntegral U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U)
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma)
    (sigma : Gal(Omega/U.functionField)) :
    genericPointLiftSchemeHom W (genericPointLiftPrecomp W g sigma) =
      Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom) ≫
        genericPointLiftSchemeHom W g

theorem

stalkClosedPointTo_specMap_algEquiv

L313 ↗

EtaleFundamentalGroups.Inertia.stalkClosedPointTo_specMap_algEquiv

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem stalkClosedPointTo_specMap_algEquiv
    {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]
    (sigma : Gal(Omega/K)) :
    let s := Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom)
    let x : Spec (.of Omega) := IsLocalRing.closedPoint Omega
    let hclosed : s x = x :=
      IsLocalRing.comap_closedPoint sigma.toRingEquiv.toRingHom
    Scheme.stalkClosedPointTo s =
      ((Spec (.of Omega)).presheaf.stalkCongr
          (.of_eq hclosed)).hom ≫
        (stalkClosedPointIso (CommRingCat.of Omega)).hom ≫
          CommRingCat.ofHom sigma.toRingEquiv.toRingHom := by
  let s := Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom)
  let x : Spec (.of Omega) := IsLocalRing.closedPoint Omega
  let hclosed : s x = x :=
    IsLocalRing.comap_closedPoint sigma.toRingEquiv.toRingHom
  dsimp only
  let e := (Spec (.of Omega)).presheaf.stalkCongr (.of_eq hclosed)
  have he :
      (Spec (.of Omega)).presheaf.germ ⊤ (s x) trivial ≫ e.hom =
        (Spec (.of Omega)).presheaf.germ ⊤ x trivial := by
    exact TopCat.Presheaf.germ_stalkSpecializes
      (F := (Spec (.of Omega)).presheaf)
      (U := ⊤) (y := s x) trivial (x := x) (.of_eq hclosed.symm)
  have heinv :
      (Spec (.of Omega)).presheaf.germ ⊤ x trivial ≫ e.inv =
        (Spec (.of Omega)).presheaf.germ ⊤ (s x) trivial := by
    rw [← he, Category.assoc, e.hom_inv_id, Category.comp_id]
  have : IsIso
      ((Spec (.of Omega)).presheaf.germ ⊤ x trivial) := by
    dsimp only [x]
    rw [← ΓSpecIso_hom_stalkClosedPointIso_inv (.of Omega)]
    infer_instance
  apply (cancel_epi
    ((Spec (.of Omega)).presheaf.germ ⊤ x trivial ≫ e.inv)).1
  calc
    ((Spec (.of Omega)).presheaf.germ ⊤ x trivial ≫ e.inv) ≫
          Scheme.stalkClosedPointTo s =
        (Spec (.of Omega)).presheaf.germ ⊤ (s x) trivial ≫
          Scheme.stalkClosedPointTo s := by rw [heinv]
    _ = (Scheme.ΓSpecIso (.of Omega)).hom ≫
          CommRingCat.ofHom sigma.toRingEquiv.toRingHom :=
      Scheme.germ_stalkClosedPointTo_Spec _
    _ = (Spec (.of Omega)).presheaf.germ ⊤ x trivial ≫
          (stalkClosedPointIso (.of Omega)).hom ≫
            CommRingCat.ofHom sigma.toRingEquiv.toRingHom := by
      dsimp only [x]
      have hfac := germ_stalkClosedPointIso_hom (.of Omega)
      exact (congrArg (fun r ↦ r ≫
        CommRingCat.ofHom sigma.toRingEquiv.toRingHom) hfac).symm
    _ = ((Spec (.of Omega)).presheaf.germ ⊤ x trivial ≫ e.inv) ≫
          (e.hom ≫ (stalkClosedPointIso (.of Omega)).hom ≫
            CommRingCat.ofHom sigma.toRingEquiv.toRingHom) := by simp

theorem

finiteEtaleGenericHomFunctionFieldAlgHom_precomp

L369 ↗

EtaleFundamentalGroups.Inertia.finiteEtaleGenericHomFunctionFieldAlgHom_precomp

Documentation

The function-field embedding associated to a precomposed generic lift is the original embedding followed by the absolute Galois automorphism.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem finiteEtaleGenericHomFunctionFieldAlgHom_precomp
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    {Omega : Type u} [Field Omega] [Algebra U.functionField Omega]
    (W : FiniteEtale U) [IsConnected W]
    (g : Over.mk (U.genericExtensionMorphism Omega) ⟶ W.toComma)
    (sigma : Gal(Omega/U.functionField)) :
    letI : IsIntegral W.left :=
      isIntegral_left_of_isConnected_finiteEtale W
    letI : Algebra U.functionField W.left.functionField :=
      finiteEtaleFunctionFieldAlgebra W
    finiteEtaleGenericHomFunctionFieldAlgHom W
        (genericPointLiftPrecomp W g sigma) =
      sigma.toAlgHom.comp (finiteEtaleGenericHomFunctionFieldAlgHom W g) := by
  let : IsIntegral W.left :=
    isIntegral_left_of_isConnected_finiteEtale W
  let : Algebra U.functionField W.left.functionField :=
    finiteEtaleFunctionFieldAlgebra W
  let q := genericPointLiftSchemeHom W g
  let qSigma := genericPointLiftSchemeHom W
    (genericPointLiftPrecomp W g sigma)
  have hq : q (IsLocalRing.closedPoint Omega) = genericPoint W.left :=
    genericPointLiftSchemeHom_genericPoint W g
  have hqSigma : qSigma (IsLocalRing.closedPoint Omega) =
      genericPoint W.left :=
    genericPointLiftSchemeHom_genericPoint W
      (genericPointLiftPrecomp W g sigma)
  have hqSigmaEq : qSigma =
      Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom) ≫ q :=
    genericPointLiftSchemeHom_precomp W g sigma
  subst qSigma
  let s := Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom)
  let x : Spec (.of Omega) := IsLocalRing.closedPoint Omega
  have hclosed : s x = x :=
    IsLocalRing.comap_closedPoint sigma.toRingEquiv.toRingHom
  change q x = genericPoint W.left at hq
  change (s ≫ q) x = genericPoint W.left at hqSigma
  change q (s x) = genericPoint W.left at hqSigma
  apply AlgHom.ext
  intro z
  change (((W.left.presheaf.stalkCongr (.of_eq hqSigma.symm)).hom ≫
      Scheme.stalkClosedPointTo (s ≫ q)).hom z) =
    sigma (((W.left.presheaf.stalkCongr (.of_eq hq.symm)).hom ≫
      Scheme.stalkClosedPointTo q).hom z)
  rw [Scheme.stalkClosedPointTo_comp]
  rw [stalkClosedPointTo_specMap_algEquiv sigma]
  rw [Scheme.Hom.stalkMap_congr_point_assoc q
    (s x) x hclosed]
  simp only [TopCat.Presheaf.stalkCongr_hom]
  have hstalk := TopCat.Presheaf.stalkSpecializes_comp_assoc W.left.presheaf
    (specializes_of_eq (congrArg q hclosed.symm)) (specializes_of_eq hqSigma)
    (q.stalkMap x ≫ (stalkClosedPointIso (.of Omega)).hom ≫
      CommRingCat.ofHom sigma.toRingEquiv.toRingHom)
  exact (congrArg
    (fun k : W.left.functionField ⟶ CommRingCat.of Omega => k.hom z) hstalk).trans
    (by rfl)

def

absoluteNormalizationPrimeInertiaSource

L430 ↗

EtaleFundamentalGroups.Inertia.absoluteNormalizationPrimeInertiaSource

Documentation

The canonical absolute divisorial inertia source in the geometric fundamental group. It is the image of inertia at one fixed prime of the absolute normalization.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

def absoluteNormalizationPrimeInertiaSource
    {U : Scheme.{u}} [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    {A : Type u} [CommRing A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    (Q : Ideal (integralClosure A Omega)) :
    Subgroup (π₁ᵉᵗ(U.genericExtensionMorphism Omega))

theorem

mem_absoluteNormalizationPrimeInertiaSource_iff

L448 ↗

EtaleFundamentalGroups.Inertia.mem_absoluteNormalizationPrimeInertiaSource_iff

Documentation

Membership in the canonical source is witnessed by one absolute Galois inertia element.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem mem_absoluteNormalizationPrimeInertiaSource_iff
    {U : Scheme.{u}} [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    {A : Type u} [CommRing A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    (Q : Ideal (integralClosure A Omega))
    (gamma : π₁ᵉᵗ(U.genericExtensionMorphism Omega)) :
    letI : MulSemiringAction Gal(Omega/U.functionField)
        (integralClosure A Omega) :=
      IsIntegralClosure.MulSemiringAction A U.functionField Omega
        (integralClosure A Omega)
    gamma ∈ absoluteNormalizationPrimeInertiaSource Omega Q ↔
      ∃ sigma : Gal(Omega/U.functionField),
        sigma ∈ Q.toAddSubgroup.inertia Gal(Omega/U.functionField) ∧
          absoluteGenericGaloisToFundamentalGroup U Omega sigma = gamma := by
  let : MulSemiringAction Gal(Omega/U.functionField)
      (integralClosure A Omega) :=
    IsIntegralClosure.MulSemiringAction A U.functionField Omega
      (integralClosure A Omega)
  change gamma ∈ Subgroup.map
      (absoluteGenericGaloisToFundamentalGroup U Omega)
      (Q.toAddSubgroup.inertia Gal(Omega/U.functionField)) ↔ _
  rfl

theorem

absoluteNormalizationPrimeInertiaSource_le_range

L476 ↗

EtaleFundamentalGroups.Inertia.absoluteNormalizationPrimeInertiaSource_le_range

Documentation

The canonical absolute inertia source lies in the range of the absolute Galois-to-fundamental-group map.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem absoluteNormalizationPrimeInertiaSource_le_range
    {U : Scheme.{u}} [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    {A : Type u} [CommRing A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    (Q : Ideal (integralClosure A Omega)) :
    absoluteNormalizationPrimeInertiaSource Omega Q ≤
      (absoluteGenericGaloisToFundamentalGroup U Omega).range

theorem

exists_absolute_inertia_restriction_of_mem_source

L500 ↗

EtaleFundamentalGroups.Inertia.exists_absolute_inertia_restriction_of_mem_source

Documentation

An element of the canonical absolute source has one absolute inertia witness whose restriction to every supplied finite normal subextension lies in inertia at the contracted normalization prime.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · full declaration

theorem exists_absolute_inertia_restriction_of_mem_source
    {U : Scheme.{u}} [IsIntegral U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega] [IsSepClosure U.functionField Omega]
    {A : Type u} [CommRing A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    {L : Type u} [Field L]
    [Algebra U.functionField L] [Algebra A L]
    [IsScalarTower A U.functionField L]
    [FiniteDimensional U.functionField L]
    [_root_.IsGalois U.functionField L]
    [Algebra L Omega] [IsScalarTower U.functionField L Omega]
    [IsScalarTower A L Omega]
    (Q : Ideal (integralClosure A Omega)) [Q.IsPrime]
    (gamma : π₁ᵉᵗ(U.genericExtensionMorphism Omega))
    (hgamma : gamma ∈ absoluteNormalizationPrimeInertiaSource Omega Q) :
    letI : MulSemiringAction Gal(Omega/U.functionField)
        (integralClosure A Omega) :=
      IsIntegralClosure.MulSemiringAction A U.functionField Omega
        (integralClosure A Omega)
    letI : MulSemiringAction Gal(L/U.functionField)
        (integralClosure A L) :=
      IsIntegralClosure.MulSemiringAction A U.functionField L
        (integralClosure A L)
    ∃ sigma : Gal(Omega/U.functionField),
      sigma ∈ Q.toAddSubgroup.inertia Gal(Omega/U.functionField) ∧
        absoluteGenericGaloisToFundamentalGroup U Omega sigma = gamma ∧
          AlgEquiv.restrictNormalHom
              (F := U.functionField) (K₁ := Omega) L sigma ∈
            (absoluteNormalizationPrimeContraction
              (A := A) (L := L) (Omega := Omega) Q).toAddSubgroup.inertia
                Gal(L/U.functionField) := by
  let : MulSemiringAction Gal(Omega/U.functionField)
      (integralClosure A Omega) :=
    IsIntegralClosure.MulSemiringAction A U.functionField Omega
      (integralClosure A Omega)
  let : MulSemiringAction Gal(L/U.functionField)
      (integralClosure A L) :=
    IsIntegralClosure.MulSemiringAction A U.functionField L
      (integralClosure A L)
  rcases (mem_absoluteNormalizationPrimeInertiaSource_iff
    Omega Q gamma).mp hgamma with ⟨sigma, hsigma, hmap⟩
  refine ⟨sigma, hsigma, hmap, ?_⟩
  apply absoluteNormalizationPrime_inertia_map_le_contraction
    (A := A) (K := U.functionField) (L := L) (Omega := Omega) Q
  exact ⟨sigma, hsigma, rfl⟩

Module documentation

Absolute generic inertia and finite function-field quotients

Declarations