Nyll.EtaleFundamentalGroups.Ramification.Product.Coordinate

theorem

productCoordinatePrime_ramificationIdx_eq

EtaleFundamentalGroups.productCoordinatePrime_ramificationIdx_eq

Documentation

Ramification at a prime selecting one product coordinate is exactly ramification at the maximal ideal of that coordinate.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uι uA
variable {R : Type uR} [CommRing R]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ j, CommRing (A j)] [∀ j, IsLocalRing (A j)]
variable [∀ j, Algebra R (A j)]

Lean source · statement

theorem productCoordinatePrime_ramificationIdx_eq (i : ι) :
    (productCoordinatePrime A i).ramificationIdx R =
      (IsLocalRing.maximalIdeal (A i)).ramificationIdx R

theorem

ringEquivProductCoordinatePrime_ramificationIdx_eq

L67 ↗

EtaleFundamentalGroups.ringEquivProductCoordinatePrime_ramificationIdx_eq

Documentation

Ramification is unchanged when a product-coordinate localization is pulled back along a ring equivalence.

Source context 12 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uι uA
variable {R : Type uR} [CommRing R]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ j, CommRing (A j)] [∀ j, IsLocalRing (A j)]
variable [∀ j, Algebra R (A j)]
section RingEquivTransport
universe uU uB
variable {U : Type uU} [CommRing U] [Algebra R U]
variable (B : ι → Type uB)
variable [∀ j, CommRing (B j)] [∀ j, IsLocalRing (B j)]

Lean source · full declaration

theorem ringEquivProductCoordinatePrime_ramificationIdx_eq
    (e : U ≃+* (∀ j, B j)) (i : ι) :
    letI : Algebra U (B i) := ringEquivProductCoordinateAlgebra B i e
    letI : Algebra R (B i) :=
      ringEquivProductCoordinateBaseAlgebra (R := R) B i e
    (ringEquivProductCoordinatePrime B i e).ramificationIdx R =
      (IsLocalRing.maximalIdeal (B i)).ramificationIdx R := by
  let q := ringEquivProductCoordinatePrime B i e
  let : Algebra U (B i) := ringEquivProductCoordinateAlgebra B i e
  let : Algebra R (B i) :=
    ringEquivProductCoordinateBaseAlgebra (R := R) B i e
  let : IsScalarTower R U (B i) :=
    ringEquivProductCoordinate_isScalarTower (R := R) B i e
  let : IsLocalization q.primeCompl (B i) :=
    ringEquivProductCoordinate_isLocalization B i e
  have hdisj : Disjoint (q.primeCompl : Set U) (q : Set U) :=
    disjoint_compl_left
  have hram := ramificationIdx_map_eq_of_isLocalization
    (R := R) (S := U) (R' := R) (S' := B i)
    (IsUnit.submonoid R) q.primeCompl q hdisj
  rw [ringEquivProductCoordinatePrime_map B i e] at hram
  exact hram.symm

Coordinate.lean

Module documentation

Ramification in a selected product coordinate

productCoordinatePrime_ramificationIdx_eq

ringEquivProductCoordinatePrime_ramificationIdx_eq

Module documentation

Ramification in a selected product coordinate

Declarations

productCoordinatePrime_ramificationIdx_eq

ringEquivProductCoordinatePrime_ramificationIdx_eq