NYLL
Module

SquareRamification.lean

Nyll.SchemeTheory.RingTheory.Ramification.Etale.SquareRamification
2 declarations indexed from sourceView source ↗

Module documentation

Ramification in an etale square

Suppose a ring in the upper-right corner is etale over the upper-left corner, while the lower-right corner is etale over the lower-left corner. For one prime in the lower-right corner and its contraction to the lower-left corner, the two horizontal ramification indices agree.

This form does not mention a tensor presentation. It is therefore suited to an actual compositum normalization after the relevant connected generic component has already been selected.

Imports2
  • Mathlib.RingTheory.RamificationInertia.Ramification
  • Mathlib.RingTheory.Smooth.Flat
Imported by4

Declarations

theorem

ramificationIdx_eq_of_formallyUnramified_flat_square

L35 ↗
EtaleFundamentalGroups.ramificationIdx_eq_of_formallyUnramified_flat_square
Documentation

Ramification indices agree across a commutative square whose two vertical maps are essentially of finite type and formally unramified, and whose right vertical map is flat.

This is the local form needed for prime localizations of etale scheme stalks: those maps need not be finitely presented.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uB uC uS
Lean source · statement
theorem ramificationIdx_eq_of_formallyUnramified_flat_square
    {R : Type uR} {B : Type uB} {C : Type uC} {S : Type uS}
    [CommRing R] [CommRing B] [CommRing C] [CommRing S]
    [Algebra R B] [Algebra R C]
    [Algebra B S] [Algebra C S] [Algebra R S]
    [IsScalarTower R B S] [IsScalarTower R C S]
    [Algebra.EssFiniteType R C] [Algebra.FormallyUnramified R C]
    [Algebra.EssFiniteType B S] [Algebra.FormallyUnramified B S]
    [Module.Flat B S]
    (q : Ideal B) [q.IsPrime]
    (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q] :
    Q.ramificationIdx C = q.ramificationIdx R
theorem

ramificationIdx_eq_of_etale_square

L96 ↗
EtaleFundamentalGroups.ramificationIdx_eq_of_etale_square
Documentation

Ramification indices agree across a commutative square whose two vertical maps are etale.

The prime q is the literal contraction of Q through B → S, expressed by its LiesOver instance. No residue-degree, tensor-kernel, or component comparison is required.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uB uC uS
Lean source · statement
theorem ramificationIdx_eq_of_etale_square
    {R : Type uR} {B : Type uB} {C : Type uC} {S : Type uS}
    [CommRing R] [CommRing B] [CommRing C] [CommRing S]
    [Algebra R B] [Algebra R C]
    [Algebra B S] [Algebra C S] [Algebra R S]
    [IsScalarTower R B S] [IsScalarTower R C S]
    [Algebra.Etale R C] [Algebra.Etale B S]
    (q : Ideal B) [q.IsPrime]
    (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q] :
    Q.ramificationIdx C = 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.