NYLL
Module

FiniteLevelEtaleDiagram.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelEtaleDiagram
11 declarations indexed from sourceView source ↗

Module documentation

The actual diagram of finite-level principal étale neighborhoods

Every object is the native principal localization constructed in the neighborhood index. Native localization lifts provide the transition maps and the maps to the literal upper invariant prime localization. Their generator formulas prove the functor and cocone laws by localization extensionality. The stages retain the commutative algebra structures used by their supplied étaleness proofs.

Imports10
Imported by3

Declarations

def

awayMap

L38 ↗
EtaleFundamentalGroups.Inertia.awayMap
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def awayMap {A : Type*} [CommRing A]
    (R S : CommAlgCat A)
    (f : R →ₐ[A] S) (r : R) (s : S) (h : f r ∣ s) :
    localizationAwayCommAlgCat A R r →ₐ[A] localizationAwayCommAlgCat A S s
theorem

awayMap_apply

L47 ↗
EtaleFundamentalGroups.Inertia.awayMap_apply
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem awayMap_apply {A : Type*} [CommRing A]
    (R S : CommAlgCat A)
    (f : R →ₐ[A] S) (r : R) (s : S) (h : f r ∣ s) (x : R) :
    awayMap R S f r s h (algebraMap R (Localization.Away r) x) =
      algebraMap S (Localization.Away s) (f x)
theorem

awayHom_ext

L56 ↗
EtaleFundamentalGroups.Inertia.awayHom_ext
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem awayHom_ext {A R B : Type*}
    [CommRing A] [CommRing R] [Semiring B] [Algebra A R] [Algebra A B]
    (r : R) (f g : localizationAwayCommAlgCat A R r →ₐ[A] B)
    (h : ∀ x : R, f (algebraMap R (Localization.Away r) x) =
      g (algebraMap R (Localization.Away r) x)) : f = g
def

awayToPrime

L66 ↗
EtaleFundamentalGroups.Inertia.awayToPrime
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def awayToPrime {A R S : Type*}
    [CommRing A] [CommRing R] [CommRing S] [Algebra A R] [Algebra A S]
    (f : R →ₐ[A] S) (r : R) (p : Ideal S) [p.IsPrime] (h : f r ∉ p) :
    localizationAwayCommAlgCat A R r →ₐ[A] Localization.AtPrime p
theorem

awayToPrime_apply

L75 ↗
EtaleFundamentalGroups.Inertia.awayToPrime_apply
Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem awayToPrime_apply {A : Type*} [CommRing A]
    (R S : CommAlgCat A)
    (f : R →ₐ[A] S) (r : R) (p : Ideal S) [p.IsPrime] (h : f r ∉ p) (x : R) :
    awayToPrime (A := A) (R := R) (S := S) f r p h
      (algebraMap R (Localization.Away r) x) =
      algebraMap S (Localization.AtPrime p) (f x)
def

finiteLevelEtaleNeighborhoodMap

L102 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleNeighborhoodMap
Documentation

The native transition map of actual principal étale neighborhoods.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
Lean source · statement
def finiteLevelEtaleNeighborhoodMap {X Y : N} (h : X ≤ Y) :
    localizationAwayCommAlgCat A (finiteLevelInertiaSubalgebra A K L Q X.level)
        X.denominator →ₐ[A]
      localizationAwayCommAlgCat A (finiteLevelInertiaSubalgebra A K L Q Y.level)
        Y.denominator
theorem

finiteLevelEtaleNeighborhoodMap_algebraMap

L122 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleNeighborhoodMap_algebraMap
Documentation

The transition map is the literal finite normalization inclusion on coefficients.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
Lean source · statement
theorem finiteLevelEtaleNeighborhoodMap_algebraMap {X Y : N} (h : X ≤ Y)
    (x : finiteLevelInertiaSubalgebra A K L Q X.level) :
    finiteLevelEtaleNeighborhoodMap A K L Q h
        (algebraMap (finiteLevelInertiaSubalgebra A K L Q X.level)
          (Localization.Away X.denominator) x) =
      algebraMap (finiteLevelInertiaSubalgebra A K L Q Y.level)
        (Localization.Away Y.denominator)
        (finiteLevelInertiaSubalgebraMap A K L Q (E := X.level) (F := Y.level) h.choose x)
def

finiteLevelEtaleDiagram

L143 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleDiagram
Documentation

The actual principal étale neighborhood diagram in commutative algebras over the original base.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
Lean source · full declaration
def finiteLevelEtaleDiagram : N ⥤ CommAlgCat.{w} A where
  obj X := localizationAwayCommAlgCat A
    (finiteLevelInertiaSubalgebra A K L Q X.level) X.denominator
  map h := CommAlgCat.ofHom (finiteLevelEtaleNeighborhoodMap A K L Q h.le)
  map_id X := by
    apply CommAlgCat.hom_ext
    apply awayHom_ext (A := A) (R := finiteLevelInertiaSubalgebra A K L Q X.level)
      X.denominator
    intro x
    change finiteLevelEtaleNeighborhoodMap A K L Q (le_refl X)
      (algebraMap _ (Localization.Away X.denominator) x) =
        algebraMap _ (Localization.Away X.denominator) x
    rw [finiteLevelEtaleNeighborhoodMap_algebraMap]
    rfl
  map_comp {X Y Z} h k := by
    apply CommAlgCat.hom_ext
    apply awayHom_ext (A := A) (R := finiteLevelInertiaSubalgebra A K L Q X.level)
      X.denominator
    intro x
    change finiteLevelEtaleNeighborhoodMap A K L Q (h.le.trans k.le)
        (algebraMap _ (Localization.Away X.denominator) x) =
      finiteLevelEtaleNeighborhoodMap A K L Q k.le
        (finiteLevelEtaleNeighborhoodMap A K L Q h.le
          (algebraMap _ (Localization.Away X.denominator) x))
    rw [finiteLevelEtaleNeighborhoodMap_algebraMap,
      finiteLevelEtaleNeighborhoodMap_algebraMap,
      finiteLevelEtaleNeighborhoodMap_algebraMap]
    rfl
def

finiteLevelEtaleNeighborhoodInclusion

L176 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleNeighborhoodInclusion
Documentation

The native map to the literal upper invariant prime localization.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
variable [Q.IsPrime]

/- The upper map retains the literal accepted localization vertex. -/
Lean source · statement
def finiteLevelEtaleNeighborhoodInclusion (X : N) :
    localizationAwayCommAlgCat A (finiteLevelInertiaSubalgebra A K L Q X.level)
        X.denominator →ₐ[A]
      (finiteLevelInertiaLocalizationCocone A K L Q).pt
theorem

finiteLevelEtaleNeighborhoodInclusion_algebraMap

L189 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleNeighborhoodInclusion_algebraMap
Documentation

The upper map is the literal normalization inclusion on coefficients.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
variable [Q.IsPrime]

/- The upper map retains the literal accepted localization vertex. -/
Lean source · statement
theorem finiteLevelEtaleNeighborhoodInclusion_algebraMap (X : N)
    (x : finiteLevelInertiaSubalgebra A K L Q X.level) :
    finiteLevelEtaleNeighborhoodInclusion A K L Q X
        (algebraMap (finiteLevelInertiaSubalgebra A K L Q X.level)
          (Localization.Away X.denominator) x) =
      algebraMap CI (Localization.AtPrime (inertiaInvariantPrime A K L Q))
        (finiteLevelInertiaSubalgebraInclusion A K L Q X.level x)
def

finiteLevelEtaleCocone

L207 ↗
EtaleFundamentalGroups.Inertia.finiteLevelEtaleCocone
Documentation

The actual étale stages form a cocone with the already constructed upper invariant localization as vertex.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits SchemeTheory
namespace EtaleFundamentalGroups.Inertia
universe u v w
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))
local notation "N" => FiniteLevelEtaleNeighborhood A K L Q
local notation "C" => integralClosure A L
local notation "CI" => FixedPoints.subalgebra A C (Q.inertia Gal(L/K))

/- The field inclusion, divisor proof and coefficient algebra owners are
fixed before the native localization-map specialization. -/
variable [Q.IsPrime]

/- The upper map retains the literal accepted localization vertex. -/
Lean source · full declaration
def finiteLevelEtaleCocone : Cocone
    (finiteLevelEtaleDiagram A K L Q ⋙ forget₂ (CommAlgCat.{w} A) (AlgCat.{w} A)) where
  pt := (finiteLevelInertiaLocalizationCocone A K L Q).pt
  ι.app X := AlgCat.ofHom (finiteLevelEtaleNeighborhoodInclusion A K L Q X)
  ι.naturality X Y h := by
    apply AlgCat.hom_ext
    apply awayHom_ext (A := A) (R := finiteLevelInertiaSubalgebra A K L Q X.level)
      X.denominator
    intro x
    change finiteLevelEtaleNeighborhoodInclusion A K L Q Y
        (finiteLevelEtaleNeighborhoodMap A K L Q h.le
          (algebraMap _ (Localization.Away X.denominator) x)) =
      finiteLevelEtaleNeighborhoodInclusion A K L Q X
        (algebraMap _ (Localization.Away X.denominator) x)
    rw [finiteLevelEtaleNeighborhoodMap_algebraMap,
      finiteLevelEtaleNeighborhoodInclusion_algebraMap,
      finiteLevelEtaleNeighborhoodInclusion_algebraMap]
    rfl

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