Module

AbsoluteDivisorialFiniteQuotientMembership.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteDivisorialFiniteQuotientMembership

3 declarations indexed from sourceView source ↗

Module documentation

Absolute divisorial inertia in every finite pointed quotient

One prime in the normalization inside a fixed separable closure defines an absolute inertia source in the generic etale fundamental group. Its elements land in normalization-prime ideal inertia in every pointed connected finite Galois quotient, using contraction of that same absolute prime along the function-field embedding selected by the pointed fiber.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

theorem

fieldGeometricPoint_comp_genericExtensionMorphism

L30 ↗

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

theorem

isNormalizationPrimeInertiaElementInFiniteQuotients_of_mem_absoluteNormalizationPrimeInertiaSource

L44 ↗

EtaleFundamentalGroups.Inertia.isNormalizationPrimeInertiaElementInFiniteQuotients_of_mem_absoluteNormalizationPrimeInertiaSource

Documentation

Membership in one absolute normalization-prime inertia source implies the finite-quotient normalization-prime inertia condition at its base prime. The normalization prime in every quotient is the literal contraction of the fixed absolute prime along the embedding selected by the pointed fiber.

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
  isNormalizationPrimeInertiaElementInFiniteQuotients_of_mem_absoluteNormalizationPrimeInertiaSource
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega]
    [IsSepClosure U.functionField Omega] [IsSepClosed Omega]
    {A : Type u} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A Omega)) [Q.IsPrime] [Q.LiesOver P]
    (gamma : π₁ᵉᵗ(U.genericExtensionMorphism Omega))
    (hgamma : gamma ∈ absoluteNormalizationPrimeInertiaSource Omega Q) :
    IsNormalizationPrimeInertiaElementInFiniteQuotients
      (U.genericExtensionMorphism Omega) P gamma

theorem

isConj_inv_of_mem_absoluteNormalizationPrimeInertiaSource_of_geometricallyIntegral_divisor

L129 ↗

EtaleFundamentalGroups.Inertia.isConj_inv_of_mem_absoluteNormalizationPrimeInertiaSource_of_geometricallyIntegral_divisor

Documentation

An element of one fixed absolute normalization-prime inertia source at a geometrically integral height-one divisor is conjugate to its inverse in the full etale fundamental group.

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 isConj_inv_of_mem_absoluteNormalizationPrimeInertiaSource_of_geometricallyIntegral_divisor
    (k : Type u) [Field k] (ek : k ≃+* ℚ)
    {U : Scheme.{u}} [IsIntegral U] [IsNormalIntegral U]
    [IsLocallyNoetherian U]
    (Omega : Type u) [Field Omega]
    [Algebra U.functionField Omega]
    [IsSepClosure U.functionField Omega] [IsSepClosed Omega]
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularRing A]
    [IsIntegrallyClosed A]
    [Algebra A U.functionField] [IsFractionRing A U.functionField]
    [Algebra A Omega] [IsScalarTower A U.functionField Omega]
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    [Algebra k (A ⧸ P)]
    (hgeo : GeometricallyIntegral
      (Spec.map (CommRingCat.ofHom (algebraMap k (A ⧸ P)))))
    (Q : Ideal (integralClosure A Omega)) [Q.IsPrime] [Q.LiesOver P]
    (gamma : π₁ᵉᵗ(U.genericExtensionMorphism Omega))
    (hgamma : gamma ∈ absoluteNormalizationPrimeInertiaSource Omega Q) :
    IsConj gamma gamma⁻¹

Module documentation

Absolute divisorial inertia in every finite pointed quotient

Declarations

fieldGeometricPoint_comp_genericExtensionMorphism

isNormalizationPrimeInertiaElementInFiniteQuotients_of_mem_absoluteNormalizationPrimeInertiaSource

isConj_inv_of_mem_absoluteNormalizationPrimeInertiaSource_of_geometricallyIntegral_divisor