Module

Cardinality.lean

Nyll.EtaleFundamentalGroups.Inertia.Localized.Cardinality

2 declarations indexed from sourceView source ↗

Module documentation

Inertia cardinality at a height-one normalization prime

This file passes from a height-one prime of a regular domain to its DVR localization, proves residue separability there from characteristic zero, and applies the Dedekind-domain inertia-cardinality theorem. All fraction-field maps and scalar towers are the canonical producers from FractionFieldLocalization; the instances below remain local to the individual declarations.

Imports3

Imported by9

theorem

localizedNormalizationResidue_isSeparable

L38 ↗

EtaleFundamentalGroups.localizedNormalizationResidue_isSeparable

Documentation

Characteristic zero of the original residue field makes the residue extension at the corresponding localized normalization prime separable.

Source context 10 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
attribute [local instance] Ideal.Quotient.field in
omit [IsDomain A] in

Lean source · full declaration

theorem localizedNormalizationResidue_isSeparable
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI :
        (localizedNormalizationPrime (K := K) (L := L) P Q).LiesOver
          (IsLocalRing.maximalIdeal (Localization.AtPrime P)) :=
      localizedNormalizationPrime_liesOver (K := K) (L := L) P Q
    Algebra.IsSeparable
      (Localization.AtPrime P ⧸
        IsLocalRing.maximalIdeal (Localization.AtPrime P))
      (integralClosure (Localization.AtPrime P) L ⧸
        localizedNormalizationPrime (K := K) (L := L) P Q) := by
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let Qlocal := localizedNormalizationPrime (K := K) (L := L) P Q
  let : Qlocal.LiesOver
      (IsLocalRing.maximalIdeal (Localization.AtPrime P)) :=
    localizedNormalizationPrime_liesOver (K := K) (L := L) P Q
  let : Qlocal.IsMaximal :=
    localizedNormalizationPrime_isMaximal (K := K) (L := L) P Q
  let : CharZero
      (Localization.AtPrime P ⧸
        IsLocalRing.maximalIdeal (Localization.AtPrime P)) :=
    charZero_of_injective_algebraMap
      (FaithfulSMul.algebraMap_injective
        (A ⧸ P)
        (Localization.AtPrime P ⧸
          IsLocalRing.maximalIdeal (Localization.AtPrime P)))
  exact Algebra.IsSeparable.of_integral _ _

theorem

localizedNormalizationInertia_card_eq_ramificationIdx

L75 ↗

EtaleFundamentalGroups.localizedNormalizationInertia_card_eq_ramificationIdx