Module

Equiv.lean

Nyll.EtaleFundamentalGroups.Ramification.BaseChange.Equiv

3 declarations indexed from sourceView source ↗

Module documentation

Ramification indices under equivalent integral models

Equivalent base and target rings do not change ramification indices. These lemmas package the change of local model needed when one divisorial valuation is represented in different scheme stalks.

Imports1

Nyll.EtaleFundamentalGroups.Normalization.Primes.AtLargerPrime

Imported by2

theorem

ramificationIdx_map_eq_of_algEquiv

L24 ↗

EtaleFundamentalGroups.ramificationIdx_map_eq_of_algEquiv

Documentation

An algebra equivalence of target rings preserves ramification indices.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uT uU

Lean source · statement

theorem ramificationIdx_map_eq_of_algEquiv
    {R : Type uR} {T : Type uT} {U : Type uU}
    [CommRing R] [CommRing T] [CommRing U]
    [Algebra R T] [Algebra R U]
    (e : T ≃ₐ[R] U) (q : Ideal T) [q.IsPrime] :
    (q.map e.toRingEquiv.toRingHom).ramificationIdx R =
      q.ramificationIdx R

theorem

ramificationIdx_eq_of_compatible_baseRingEquiv

L50 ↗

EtaleFundamentalGroups.ramificationIdx_eq_of_compatible_baseRingEquiv

Documentation

Replacing a base ring by an equivalent compatible model preserves the ramification index of every prime of a fixed target ring.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uT uU

Lean source · statement

theorem ramificationIdx_eq_of_compatible_baseRingEquiv
    {R : Type uR} {S : Type uS} {U : Type uU}
    [CommRing R] [CommRing S] [CommRing U]
    [Algebra R U] [Algebra S U]
    (e : R ≃+* S)
    (hcompat : (algebraMap S U).comp e.toRingHom = algebraMap R U)
    (q : Ideal U) [q.IsPrime] :
    q.ramificationIdx S = q.ramificationIdx R

theorem

ramificationIdx_map_eq_of_compatible_ringEquiv

L85 ↗

EtaleFundamentalGroups.ramificationIdx_map_eq_of_compatible_ringEquiv

Documentation

Compatible equivalences of both source and target rings preserve the ramification index at corresponding target primes.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uT uU

Lean source · statement

theorem ramificationIdx_map_eq_of_compatible_ringEquiv
    {R : Type uR} {S : Type uS} {T : Type uT} {U : Type uU}
    [CommRing R] [CommRing S] [CommRing T] [CommRing U]
    [Algebra R T] [Algebra S U]
    (eBase : R ≃+* S) (eTarget : T ≃+* U)
    (hcompat : eTarget.toRingHom.comp (algebraMap R T) =
      (algebraMap S U).comp eBase.toRingHom)
    (q : Ideal T) [q.IsPrime] :
    (q.map eTarget.toRingHom).ramificationIdx S =
      q.ramificationIdx R

Module documentation

Ramification indices under equivalent integral models

Declarations

ramificationIdx_map_eq_of_algEquiv

ramificationIdx_eq_of_compatible_baseRingEquiv

ramificationIdx_map_eq_of_compatible_ringEquiv