Module

ActionComparison.lean

Nyll.EtaleFundamentalGroups.Inertia.Localized.ActionComparison

3 declarations indexed from sourceView source ↗

Module documentation

Action comparison for localized normalization inertia

The generic action on a localized normalization and the action obtained from its integral-closure universal property have the same value on every element. Consequently, the two definitions of the inertia subgroup coincide.

Imports2

Imported by2

theorem

localizationAtPrime_integralClosure_smul_eq

L34 ↗

EtaleFundamentalGroups.localizationAtPrime_integralClosure_smul_eq

Documentation

On the normalization after localization at P, the generic action and the action supplied by the integral-closure construction agree pointwise.

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]
variable [Algebra.IsAlgebraic K L]
omit [Algebra A L] [IsScalarTower A K L] in

Lean source · full declaration

theorem localizationAtPrime_integralClosure_smul_eq
    (P : Ideal A) [P.IsPrime] :
    let V := Localization.AtPrime P
    letI : Algebra V K :=
      localizationAtPrimeToFractionFieldAlgebra (K := K) P
    letI : Algebra V L :=
      localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI : IsScalarTower V K L :=
      localizationAtPrimeToFractionFieldToExtension_isScalarTower
        (K := K) (L := L) P
    letI : IsFractionRing V K :=
      localizationAtPrimeToFractionField_isFractionRing (K := K) P
    letI : SMulCommClass Gal(L/K) V L :=
      localizationAtPrime_galois_smulCommClass (K := K) (L := L) P
    let B := integralClosure V L
    let genericAction : MulSemiringAction Gal(L/K) B := inferInstance
    let integralClosureAction : MulSemiringAction Gal(L/K) B :=
      IsIntegralClosure.MulSemiringAction V K L B
    ∀ (sigma : Gal(L/K)) (x : B),
      (letI := genericAction; sigma • x) =
        (letI := integralClosureAction; sigma • x) := by
  let V := Localization.AtPrime P
  let : Algebra V K :=
    localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let : Algebra V L :=
    localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let : IsScalarTower V K L :=
    localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) P
  let : IsFractionRing V K :=
    localizationAtPrimeToFractionField_isFractionRing (K := K) P
  let : SMulCommClass Gal(L/K) V L :=
    localizationAtPrime_galois_smulCommClass (K := K) (L := L) P
  let B := integralClosure V L
  let genericAction : MulSemiringAction Gal(L/K) B := inferInstance
  let integralClosureAction : MulSemiringAction Gal(L/K) B :=
    IsIntegralClosure.MulSemiringAction V K L B
  change ∀ (sigma : Gal(L/K)) (x : B),
    (letI := genericAction; sigma • x) =
      (letI := integralClosureAction; sigma • x)
  intro sigma x
  apply Subtype.ext
  calc
    ((letI := genericAction; (sigma • x : B)) : L) =
        sigma • (x : L) := by
      let := genericAction
      exact integralClosure.coe_smul sigma x
    _ = sigma (x : L) := AlgEquiv.smul_def _ _
    _ = ((letI := integralClosureAction; (sigma • x : B)) : L) := by
      let := integralClosureAction
      exact (algebraMap_galRestrict_apply V sigma x).symm

def

localizedNormalizationIntegralClosureInertia

L89 ↗

EtaleFundamentalGroups.localizedNormalizationIntegralClosureInertia

Documentation

The inertia subgroup computed with the integral-closure action on the localized normalization. This named form is useful when applying results whose local action is constructed by IsIntegralClosure.MulSemiringAction.

Source context 9 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]
variable [Algebra.IsAlgebraic K L]

Lean source · statement

def localizedNormalizationIntegralClosureInertia
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) :
    Subgroup Gal(L/K)

theorem

localizedNormalizationInertia_eq_integralClosureInertia

L113 ↗

EtaleFundamentalGroups.localizedNormalizationInertia_eq_integralClosureInertia

Documentation

Localized normalization inertia is independent of whether its action is obtained by restricting the generic action or by the integral-closure construction.

Source context 9 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]
variable [Algebra.IsAlgebraic K L]

Lean source · statement

theorem localizedNormalizationInertia_eq_integralClosureInertia
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) :
    localizedNormalizationInertia (K := K) (L := L) P Q =
      localizedNormalizationIntegralClosureInertia
        (K := K) (L := L) P Q

Module documentation

Action comparison for localized normalization inertia

Declarations

localizationAtPrime_integralClosure_smul_eq

localizedNormalizationIntegralClosureInertia

localizedNormalizationInertia_eq_integralClosureInertia