NYLL
Module

Flat.lean

Nyll.SchemeTheory.RingTheory.Ramification.BaseChange.Flat
2 declarations indexed from sourceView source ↗

Module documentation

Ramification indices in a flat base-change square

If both vertical maps in a commutative square are faithfully flat and the chosen primes are exactly the extensions of the original primes, then the ramification index is unchanged across the square. The proof compares the two ramification-index tower formulas; the two vertical indices are one because their defining ideals map onto the chosen primes.

Imports2
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  • Mathlib.RingTheory.RamificationInertia.Ramification
Imported by2

Declarations

theorem

ramificationIdx_eq_one_of_map_eq

L29 ↗
EtaleFundamentalGroups.ramificationIdx_eq_one_of_map_eq
Documentation

A prime which is exactly the extension of the prime below it has ramification index one. This elementary form does not require the algebra map to be essentially of finite type.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
Lean source · statement
theorem ramificationIdx_eq_one_of_map_eq
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    (p : Ideal R) (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (hmap : p.map (algebraMap R S) = q) :
    q.ramificationIdx R = 1
theorem

ramificationIdx_eq_of_flat_baseChange_mapped_primes

L55 ↗
EtaleFundamentalGroups.ramificationIdx_eq_of_flat_baseChange_mapped_primes
Documentation

Ramification indices are unchanged in a flat commutative square when the selected vertical primes are their scheme-theoretic extensions.

Faithful flatness supplies the two vertical LiesOver instances. The only remaining prime comparison is the horizontal one in the upper row.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uR' uS'
Lean source · statement
theorem ramificationIdx_eq_of_flat_baseChange_mapped_primes
    {R : Type uR} {S : Type uS} {R' : Type uR'} {S' : Type uS'}
    [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S']
    [Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S']
    [Module.FaithfullyFlat R R'] [Module.FaithfullyFlat S S']
    [Module.Flat R' S']
    (p : Ideal R) (q : Ideal S) [q.IsPrime] [q.LiesOver p]
    (p' : Ideal R') (q' : Ideal S') [q'.IsPrime] [q'.LiesOver p']
    (hpmap : p.map (algebraMap R R') = p')
    (hqmap : q.map (algebraMap S S') = q') :
    q'.ramificationIdx R' = q.ramificationIdx R

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