NYLL
Module

FiniteLevelEtaleNeighborhoods.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelEtaleNeighborhoods
10 declarations indexed from sourceView source ↗

Module documentation

Actual finite-level principal étale neighborhoods

The finite-Galois normalization theorem supplies an étale denominator at each actual invariant stage. Multiplying it by any prescribed denominator outside the contracted prime gives a further étale neighborhood. These neighborhoods form a nonempty directed preorder: at a common finite Galois level, multiply an étale denominator by the two transported denominators.

The transition condition uses divisibility of the literal transported denominator. It therefore supplies the unit needed by the native Away map. This file constructs the actual index and its filteredness; the diagram and its colimit are separate declarations.

Imports14
Imported by4

Declarations

def

awayEquiv

L48 ↗
EtaleFundamentalGroups.Inertia.awayEquiv
Source context 4 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
Lean source · statement
def awayEquiv {A : Type u} {R : Type v} {S : Type w}
    [CommRing A] [CommRing R] [CommRing S] [Algebra A R] [Algebra A S]
    (e : R ≃ₐ[A] S) (f : R) :
    localizationAwayCommAlgCat A R f ≃ₐ[A] localizationAwayCommAlgCat A S (e f)
theorem

etale_away_mul

L56 ↗
EtaleFundamentalGroups.Inertia.etale_away_mul
Source context 4 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
Lean source · statement
theorem etale_away_mul {A : Type u} {R : Type w}
    [CommRing A] [CommRing R] [Algebra A R] (f d : R)
    [Algebra.Etale A (localizationAwayCommAlgCat A R f)] :
    Algebra.Etale A (localizationAwayCommAlgCat A R (f * d))
structure

FiniteLevelEtaleNeighborhood

L82 ↗
EtaleFundamentalGroups.Inertia.FiniteLevelEtaleNeighborhood
Documentation

An actual principal neighborhood at a finite invariant stage. Its étaleness is part of the object property and is constructed below from the finite-Galois normalization theorem.

Source context 6 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
Lean source · full declaration
structure FiniteLevelEtaleNeighborhood where
  /-- The actual finite Galois stage. -/
  level : FiniteGaloisIntermediateField K L
  /-- The element defining the principal open at this stage. -/
  denominator : finiteLevelInertiaSubalgebra A K L Q level
  /-- The principal open contains the contracted prime. -/
  not_mem : denominator ∉ finiteLevelInertiaPrime A K L Q level
  /-- The actual principal localization is etale over the original base. -/
  etale : Algebra.Etale A
    (localizationAwayCommAlgCat A
      (finiteLevelInertiaSubalgebra A K L Q level) denominator)
instance

(anonymous instance)

L97 ↗
Documentation

Literal finite-field inclusion together with denominator divisibility.

Source context 7 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
namespace FiniteLevelEtaleNeighborhood
Lean source · full declaration
instance : LE (FiniteLevelEtaleNeighborhood A K L Q) where
  le X Y := ∃ h : X.level ≤ Y.level,
    finiteLevelInertiaSubalgebraMap A K L Q h X.denominator ∣ Y.denominator
instance

(anonymous instance)

L101 ↗
Source context 7 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
namespace FiniteLevelEtaleNeighborhood
Lean source · full declaration
instance : Preorder (FiniteLevelEtaleNeighborhood A K L Q) where
  le_refl X := ⟨le_refl X.level, dvd_refl X.denominator⟩
  le_trans X Y Z hXY hYZ := by
    obtain ⟨hEF, hXY⟩ := hXY
    obtain ⟨hFG, hYZ⟩ := hYZ
    refine ⟨hEF.trans hFG, ?_⟩
    exact (map_dvd (finiteLevelInertiaSubalgebraMap A K L Q hFG) hXY).trans hYZ
theorem

denominator_isUnit

L111 ↗
EtaleFundamentalGroups.Inertia.FiniteLevelEtaleNeighborhood.denominator_isUnit
Documentation

Every transition makes the source denominator invertible in the target principal localization, exactly as required by Away.liftAlgHom.

Source context 7 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
namespace FiniteLevelEtaleNeighborhood
Lean source · statement
theorem denominator_isUnit {X Y : FiniteLevelEtaleNeighborhood A K L Q}
    (h : X ≤ Y) :
    ∃ hEF : X.level ≤ Y.level,
      IsUnit (algebraMap (finiteLevelInertiaSubalgebra A K L Q Y.level)
        (Localization.Away Y.denominator)
          (finiteLevelInertiaSubalgebraMap A K L Q hEF X.denominator))
theorem

finiteLevelInertia_exists_etale_away

L127 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertia_exists_etale_away
Documentation

The actual finite invariant stage has a principal neighborhood étale over the original normal domain. The comparison with finite-level inertia invariants is the proved equality of subalgebras.

Source context 7 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
variable [Q.IsPrime] [IsDomain A] [IsIntegrallyClosed A]
Lean source · statement
theorem finiteLevelInertia_exists_etale_away (E : FiniteGaloisIntermediateField K L) :
    ∃ f : finiteLevelInertiaSubalgebra A K L Q E,
      f ∉ finiteLevelInertiaPrime A K L Q E ∧
        Algebra.Etale A
          (localizationAwayCommAlgCat A (finiteLevelInertiaSubalgebra A K L Q E) f)
theorem

finiteLevelInertia_exists_etale_away_dvd

L157 ↗
EtaleFundamentalGroups.Inertia.finiteLevelInertia_exists_etale_away_dvd
Documentation

Any denominator outside the chosen prime can be inverted on a genuine finite-level principal étale neighborhood.

Source context 7 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
variable [Q.IsPrime] [IsDomain A] [IsIntegrallyClosed A]
Lean source · statement
theorem finiteLevelInertia_exists_etale_away_dvd
    (E : FiniteGaloisIntermediateField K L)
    (d : finiteLevelInertiaSubalgebra A K L Q E)
    (hd : d ∉ finiteLevelInertiaPrime A K L Q E) :
    ∃ f : finiteLevelInertiaSubalgebra A K L Q E,
      f ∉ finiteLevelInertiaPrime A K L Q E ∧
        Algebra.Etale A
          (localizationAwayCommAlgCat A (finiteLevelInertiaSubalgebra A K L Q E) f) ∧
            d ∣ f
instance

(anonymous instance)

L175 ↗
Source context 8 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
variable [Q.IsPrime] [IsDomain A] [IsIntegrallyClosed A]
namespace FiniteLevelEtaleNeighborhood
Lean source · statement
instance : Nonempty (FiniteLevelEtaleNeighborhood A K L Q)
instance

(anonymous instance)

L183 ↗
Documentation

At a common finite Galois level, the product of the two transported denominators still avoids the contracted prime. A further genuinely étale denominator supplied above gives a common refinement.

Source context 8 commands

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

noncomputable section
open CategoryTheory SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w

/- The sparse transport helpers apply native localization owners with the
literal carriers exposed. They do not install another scalar action. -/
attribute [local instance] normalizationInertiaImageAction normalizationInertiaImageTower
  normalizationInertiaCoefficientCommClass inertiaInvariantPrime_isPrime
  finiteLevelInertiaPrime_isPrime
variable (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L))
variable [Q.IsPrime] [IsDomain A] [IsIntegrallyClosed A]
namespace FiniteLevelEtaleNeighborhood
Lean source · full declaration
instance : IsDirectedOrder (FiniteLevelEtaleNeighborhood A K L Q) where
  directed X Y := by
    let E : FiniteGaloisIntermediateField K L := X.level ⊔ Y.level
    let x : finiteLevelInertiaSubalgebra A K L Q E :=
      finiteLevelInertiaSubalgebraMap A K L Q le_sup_left X.denominator
    let y : finiteLevelInertiaSubalgebra A K L Q E :=
      finiteLevelInertiaSubalgebraMap A K L Q le_sup_right Y.denominator
    have hx : x ∉ finiteLevelInertiaPrime A K L Q E := X.not_mem
    have hy : y ∉ finiteLevelInertiaPrime A K L Q E := Y.not_mem
    have hp : (finiteLevelInertiaPrime A K L Q E).IsPrime := inferInstance
    have hxy : x * y ∉ finiteLevelInertiaPrime A K L Q E := hp.mul_notMem hx hy
    obtain ⟨f, hf, hEtale, hdiv⟩ :=
      finiteLevelInertia_exists_etale_away_dvd A K L Q E (x * y) hxy
    refine ⟨⟨E, f, hf, hEtale⟩, ?_, ?_⟩
    · exact ⟨le_sup_left, (dvd_mul_right x y).trans hdiv⟩
    · exact ⟨le_sup_right, (dvd_mul_left y x).trans hdiv⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.