Module

ResidueCharacteristic.lean

Nyll.SchemeTheory.LocalGeometry.HeightTwo.ResidueCharacteristic

3 declarations indexed from sourceView source ↗

Module documentation

Residue characteristic at a prime localization

An integer which is a nonunit in a prime localization vanishes in its residue field. For a prime integer this determines the residue characteristic. We also record the canonical map from a localized branch quotient to that residue field.

Imports2

Mathlib.Algebra.CharP.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by3

theorem

map_le_maximalIdeal_localizationAtPrime

L29 ↗

EtaleFundamentalGroups.map_le_maximalIdeal_localizationAtPrime

Documentation

A branch contained in the localization prime maps into the maximal ideal of the prime localization.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem map_le_maximalIdeal_localizationAtPrime
    {A : Type u} [CommRing A]
    (q P : Ideal A) [P.IsPrime] (hqP : q ≤ P) :
    Ideal.map (algebraMap A (Localization.AtPrime P)) q ≤
      maximalIdeal (Localization.AtPrime P)

def

localizationAtPrimeBranchQuotientToResidue

L38 ↗

EtaleFundamentalGroups.localizationAtPrimeBranchQuotientToResidue

Documentation

The canonical residue map from a branch quotient after localization.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · statement

def localizationAtPrimeBranchQuotientToResidue
    {A : Type u} [CommRing A]
    (q P : Ideal A) [P.IsPrime] (hqP : q ≤ P) :
    (Localization.AtPrime P ⧸
        Ideal.map (algebraMap A (Localization.AtPrime P)) q) →+*
      (Localization.AtPrime P ⧸
        maximalIdeal (Localization.AtPrime P))

theorem

charP_localizationAtPrime_residue_of_natCast_nonunit

L50 ↗

EtaleFundamentalGroups.charP_localizationAtPrime_residue_of_natCast_nonunit

Documentation

A prime integer which is a nonunit in a prime localization is the characteristic of its residue field.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem charP_localizationAtPrime_residue_of_natCast_nonunit
    {A : Type u} [CommRing A]
    (P : Ideal A) [P.IsPrime]
    (p : ℕ) (hp : p.Prime)
    (hp_nonunit :
      ¬ IsUnit
        (algebraMap A (Localization.AtPrime P) (p : A))) :
    CharP
      (Localization.AtPrime P ⧸
        maximalIdeal (Localization.AtPrime P)) p

Module documentation

Residue characteristic at a prime localization

Declarations

map_le_maximalIdeal_localizationAtPrime

localizationAtPrimeBranchQuotientToResidue

charP_localizationAtPrime_residue_of_natCast_nonunit