Module

BaseChange.lean

Nyll.SchemeTheory.RingTheory.Ramification.Etale.BaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Ramification index under an étale tensor base change

This file records the ramification-index comparison needed after choosing an étale factor as in Stacks Project, Tag 00UJ. The contraction equality supplied by that construction is the only prime-comparison input: residue-field bijectivity, height-one hypotheses, and normalization are not needed for this step.

The nondefault algebra structure on the right tensor factor, its scalar tower, and the transferred étale structure are kept local to the proof so that importing this leaf does not add global instances.

Imports2

Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.RingTheory.Smooth.Flat

Imported by3

theorem

ramificationIdx_tensorProduct_eq_of_etale

L32 ↗

EtaleFundamentalGroups.ramificationIdx_tensorProduct_eq_of_etale

Documentation

Ramification indices are unchanged after an étale tensor base change.

Here Q is a prime of C ⊗[R] B lying over q through the right tensor-factor map. This is the precise contraction equality produced by the chosen-prime part of Tag 00UJ.

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups

Lean source · statement

theorem ramificationIdx_tensorProduct_eq_of_etale
    {R B C : Type*} [CommRing R] [CommRing B] [CommRing C]
    [Algebra R B] [Algebra R C] [Algebra.Etale R C]
    (q : Ideal B) [q.IsPrime]
    (Q : Ideal (TensorProduct R C B)) [Q.IsPrime]
    (hQ : Q.comap Algebra.TensorProduct.includeRight.toRingHom = q) :
    Q.ramificationIdx C = q.ramificationIdx R

Module documentation

Ramification index under an étale tensor base change

Declarations

ramificationIdx_tensorProduct_eq_of_etale