NYLL
Module

PrimeParameterLocalization.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.PrimeParameterLocalization
2 declarations indexed from sourceView source ↗

Module documentation

Prime boundary parameters after localization

A prime boundary parameter remains prime at every larger prime containing it, and becomes a unit at every other prime localization. In the first case, characteristic zero of its generic residue ring is preserved by the localization. These are the exact inputs needed by prime-or-unit multi-boundary unit descent.

Imports4
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Ideal
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.Algebra.CharP.Algebra
Imported by5

Declarations

theorem

prime_or_isUnit_algebraMap_localizationAtPrime

L28 ↗
EtaleFundamentalGroups.Kummer.prime_or_isUnit_algebraMap_localizationAtPrime
Documentation

A prime element is either still prime or becomes a unit after localization at a prime ideal.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
theorem prime_or_isUnit_algebraMap_localizationAtPrime
    {A : Type u} [CommRing A] [IsDomain A]
    (P : Ideal A) [P.IsPrime] {t : A} (ht : Prime t) :
    Prime (algebraMap A (Localization.AtPrime P) t) ∨
      IsUnit (algebraMap A (Localization.AtPrime P) t)
theorem

charZero_quotient_algebraMap_localizationAtPrime

L57 ↗
EtaleFundamentalGroups.Kummer.charZero_quotient_algebraMap_localizationAtPrime
Documentation

Characteristic zero along a prime divisor is preserved when localizing at a larger prime containing that divisor.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
theorem charZero_quotient_algebraMap_localizationAtPrime
    {A : Type u} [CommRing A] [IsDomain A]
    (P : Ideal A) [P.IsPrime] {t : A} (ht : Prime t)
    (htP : t ∈ P)
    (hCharZero : CharZero (A ⧸ Ideal.span {t})) :
    CharZero
      (Localization.AtPrime P ⧸
        Ideal.span {algebraMap A (Localization.AtPrime P) t})

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