Module

FiniteLevelEtaleColimit.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelEtaleColimit

5 declarations indexed from sourceView source ↗

Module documentation

The étale filtered-colimit presentation in Stacks tag 0BSU

The already constructed localized finite-level colimit supplies an actual finite-level representative. A denominator for this representative becomes a unit on a genuine principal étale neighborhood. The two literal coefficient squares and unit cancellation give its representative in the étale diagram. Equality is detected by the actual inclusions into the upper invariant localization.

Imports15

Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelEtaleDiagram
Nyll.EtaleFundamentalGroups.Inertia.FiniteLevelEtaleNeighborhoods
Nyll.SchemeTheory.RingTheory.Localization.AwayAlgebra
Nyll.SchemeTheory.RingTheory.Localization.CommAlgPrincipal
Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaLocalization
Mathlib.Algebra.Category.AlgCat.FilteredColimits
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.Algebra.Group.Units.Basic
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Mathlib.CategoryTheory.Limits.Types.Filtered
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.Defs

Imported by2

theorem

away_injective_of_coeff_injective

L43 ↗

EtaleFundamentalGroups.Inertia.away_injective_of_coeff_injective

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 · full declaration

theorem away_injective_of_coeff_injective
    {A : Type*} [CommRing A] (R : CommAlgCat A) (r : R)
    {T : Type*} [CommSemiring T]
    (j : localizationAwayCommAlgCat A R r →+* T)
    (hj : Function.Injective fun x : R => j (algebraMap R (Localization.Away r) x)) :
    Function.Injective j := by
  exact SchemeTheory.principalLocalization_injective_of_coefficient_injective
    (R := R) (T := T) r j hj

theorem

exists_preimage_of_unit_denominator

L54 ↗

EtaleFundamentalGroups.Inertia.exists_preimage_of_unit_denominator

Documentation

A denominator already made invertible supplies a preimage, using only the two actual coefficient maps and the localization's fraction equation.

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 exists_preimage_of_unit_denominator
    {A : Type*} [CommRing A] (R : CommAlgCat A)
    (p : Ideal R) [p.IsPrime] (f n : R) (d : p.primeCompl)
    (z : Localization.AtPrime p)
    (hz : z * algebraMap R (Localization.AtPrime p) d =
      algebraMap R (Localization.AtPrime p) n)
    (hd : IsUnit (algebraMap R (Localization.Away f) d))
    {U : Type*} [Semiring U]
    (j : Localization.Away f →+* U) (k : Localization.AtPrime p →+* U)
    (hcoeff : ∀ a : R, j (algebraMap R (Localization.Away f) a) =
      k (algebraMap R (Localization.AtPrime p) a)) :
    ∃ x : Localization.Away f, j x = k z

theorem

finiteLevelEtaleNeighborhoodInclusion_injective

L101 ↗

EtaleFundamentalGroups.Inertia.finiteLevelEtaleNeighborhoodInclusion_injective

Documentation

Each actual étale neighborhood embeds into the upper invariant localization. The coefficient inclusion and the upper localization are injective, and native localization extensionality supplies the result.

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)) [Q.IsPrime]
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))

Lean source · statement

theorem finiteLevelEtaleNeighborhoodInclusion_injective (X : N) :
    Function.Injective (finiteLevelEtaleNeighborhoodInclusion A K L Q X)

theorem

finiteLevelEtale_exists_rep

L137 ↗

EtaleFundamentalGroups.Inertia.finiteLevelEtale_exists_rep

Documentation

The accepted localized finite-level colimit supplies a representative; the actual étale denominator-refinement theorem then places it on one of the constructed étale neighborhoods.

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)) [Q.IsPrime]
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))
variable [IsDomain A] [IsIntegrallyClosed A]

Lean source · statement

theorem finiteLevelEtale_exists_rep
    (z : (finiteLevelInertiaLocalizationCocone A K L Q).pt) :
    ∃ (X : N) (x : (finiteLevelEtaleDiagram A K L Q).obj X),
      finiteLevelEtaleNeighborhoodInclusion A K L Q X x = z

def

finiteLevelEtaleCoconeIsColimit

L184 ↗

EtaleFundamentalGroups.Inertia.finiteLevelEtaleCoconeIsColimit

Documentation

The upper inertia-invariant prime localization is the filtered colimit of the actual finite-level principal étale neighborhoods. There is no finite-presentation assumption on the fraction field or the infinite normalization, and the cocone vertex and its coefficient maps are literal.

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)) [Q.IsPrime]
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))
variable [IsDomain A] [IsIntegrallyClosed A]

Lean source · statement

def finiteLevelEtaleCoconeIsColimit : IsColimit (finiteLevelEtaleCocone A K L Q)

Module documentation

The étale filtered-colimit presentation in Stacks tag 0BSU

Declarations

away_injective_of_coeff_injective

exists_preimage_of_unit_denominator

finiteLevelEtaleNeighborhoodInclusion_injective

finiteLevelEtale_exists_rep

finiteLevelEtaleCoconeIsColimit