NYLL
Module

IdealResidueComparison.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.IdealResidueComparison
21 declarations indexed from sourceView source ↗

Module documentation

Residue fields under localization at a normalization prime

This file compares the decomposition group and residue action attached to a prime of a normalization with the corresponding objects for the localized valuation subring. The comparison is canonical and retains the base-prime residue field.

Imports4
Imported by2

Declarations

theorem

normalizationGaloisSMulCommClass

L51 ↗
TameAbhyankar.SGA1.normalizationGaloisSMulCommClass
Documentation

The normalization action fixes the base ring.

Source context 20 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
omit [IsDedekindDomain B] in
Lean source · full declaration
theorem normalizationGaloisSMulCommClass :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    SMulCommClass Gal(L/K) A B := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  constructor
  intro sigma a b
  apply (IsFractionRing.injective B L)
  simp only [Algebra.smul_def, map_mul,
    algebraMap_normalization_smul (A := A)]
  have ha : (sigma : Gal(L/K)) (algebraMap A L a) =
      algebraMap A L a := by
    calc
      (sigma : Gal(L/K)) (algebraMap A L a) =
          (sigma : Gal(L/K))
            (algebraMap K L (algebraMap A K a)) := by
        rw [← IsScalarTower.algebraMap_apply A K L]
      _ = algebraMap K L (algebraMap A K a) :=
        (sigma : Gal(L/K)).commutes (algebraMap A K a)
      _ = algebraMap A L a :=
        (IsScalarTower.algebraMap_apply A K L a).symm
  have haB : (sigma : Gal(L/K))
        (algebraMap B L (algebraMap A B a)) =
      algebraMap B L (algebraMap A B a) := by
    calc
      (sigma : Gal(L/K))
          (algebraMap B L (algebraMap A B a)) =
        (sigma : Gal(L/K)) (algebraMap A L a) := by
          rw [IsScalarTower.algebraMap_apply A B L]
      _ = algebraMap A L a := ha
      _ = algebraMap B L (algebraMap A B a) :=
        IsScalarTower.algebraMap_apply A B L a
  rw [haB]
def

idealLocalizationRingHom

L86 ↗
TameAbhyankar.SGA1.idealLocalizationRingHom
Documentation

The canonical map from a normalization ring to the valuation ring obtained by localizing at P.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · statement
def idealLocalizationRingHom :
    B →+* idealLocalizationValuationSubring B L P hP
theorem

idealLocalizationRingHom_apply_coe

L91 ↗
TameAbhyankar.SGA1.idealLocalizationRingHom_apply_coe
Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · statement
theorem idealLocalizationRingHom_apply_coe (b : B) :
    ((idealLocalizationRingHom (B := B) (L := L) P hP b :
      idealLocalizationValuationSubring B L P hP) : L) =
      algebraMap B L b
theorem

idealLocalizationRingHom_mem_maximalIdeal_iff

L98 ↗
TameAbhyankar.SGA1.idealLocalizationRingHom_mem_maximalIdeal_iff
Documentation

Membership in P is detected by the maximal ideal after localization.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · statement
theorem idealLocalizationRingHom_mem_maximalIdeal_iff (b : B) :
    idealLocalizationRingHom (B := B) (L := L) P hP b ∈
        IsLocalRing.maximalIdeal
          (idealLocalizationValuationSubring B L P hP) ↔
      b ∈ P
theorem

idealLocalizationResidueEquiv_mk

L109 ↗
TameAbhyankar.SGA1.idealLocalizationResidueEquiv_mk
Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · statement
theorem idealLocalizationResidueEquiv_mk (b : B) :
    idealLocalizationResidueEquiv B L P hP
        (Ideal.Quotient.mk P b) =
      IsLocalRing.residue
        (idealLocalizationValuationSubring B L P hP)
        (idealLocalizationRingHom (B := B) (L := L) P hP b)
theorem

globalDecomposition_maps_localization

L117 ↗
TameAbhyankar.SGA1.globalDecomposition_maps_localization
Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
theorem globalDecomposition_maps_localization :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    ∀ (sigma : HilbertRamification.Dedekind.decompositionGroup P Gal(L/K))
      {x : L},
      x ∈ idealLocalizationValuationSubring B L P hP →
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
        idealLocalizationValuationSubring B L P hP := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma x hx
  change x ∈ idealLocalizationSubalgebra B L P at hx
  change ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
    idealLocalizationSubalgebra B L P
  rcases hx with ⟨a, s, hs, rfl⟩
  have hsigma : (sigma : Gal(L/K)) • s ∈ P.primeCompl := by
    intro hsigmaP
    have hsmul : (sigma : Gal(L/K))⁻¹ • ((sigma : Gal(L/K)) • s) ∈
        (sigma : Gal(L/K))⁻¹ • P :=
      Ideal.smul_mem_pointwise_smul
        (M := Gal(L/K)) (sigma : Gal(L/K))⁻¹
        ((sigma : Gal(L/K)) • s) P hsigmaP
    have hinvP : (sigma : Gal(L/K))⁻¹ • P = P := by
      calc
        (sigma : Gal(L/K))⁻¹ • P =
            (sigma : Gal(L/K))⁻¹ • ((sigma : Gal(L/K)) • P) :=
          congrArg ((sigma : Gal(L/K))⁻¹ • ·) sigma.property.symm
        _ = P := by simp
    have hsP : s ∈ P := by
      simpa [hinvP] using hsmul
    exact hs hsP
  refine ⟨(sigma : Gal(L/K)) • a, (sigma : Gal(L/K)) • s,
    hsigma, ?_⟩
  simp only [map_mul, map_inv₀,
    algebraMap_normalization_smul (A := A)]
theorem

globalDecomposition_maps_localization_iff

L151 ↗
TameAbhyankar.SGA1.globalDecomposition_maps_localization_iff
Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
theorem globalDecomposition_maps_localization_iff :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    ∀ (sigma : HilbertRamification.Dedekind.decompositionGroup P Gal(L/K))
      (x : L),
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
          idealLocalizationValuationSubring B L P hP ↔
        x ∈ idealLocalizationValuationSubring B L P hP := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma x
  constructor
  · intro hx
    let sigmaInv : HilbertRamification.Dedekind.decompositionGroup P Gal(L/K) :=
      sigma⁻¹
    have hinv := globalDecomposition_maps_localization
      (A := A) (P := P) (hP := hP) sigmaInv hx
    simpa [sigmaInv] using hinv
  · exact globalDecomposition_maps_localization
      (A := A) (P := P) (hP := hP) sigma
def

globalIdealDecompositionToLocalDecomposition

L172 ↗
TameAbhyankar.SGA1.globalIdealDecompositionToLocalDecomposition
Documentation

Stabilizing a normalization prime is equivalent to stabilizing its localized valuation subring, in the forward direction.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
def globalIdealDecompositionToLocalDecomposition :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    HilbertRamification.Dedekind.decompositionGroup P Gal(L/K) →*
      decompositionGroup K (idealLocalizationValuationSubring B L P hP) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  refine
    { toFun := fun sigma ↦ ⟨(sigma : Gal(L/K)), ?_⟩
      map_one' := rfl
      map_mul' := fun _ _ ↦ rfl }
  apply _root_.ValuationSubring.toSubring_injective
  ext x
  change x ∈ (sigma : Gal(L/K)) •
      idealLocalizationValuationSubring B L P hP ↔
    x ∈ idealLocalizationValuationSubring B L P hP
  rw [_root_.ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem]
  exact globalDecomposition_maps_localization_iff
    (A := A) (P := P) (hP := hP) sigma⁻¹ x
def

localDecompositionToGlobalIdealDecomposition

L192 ↗
TameAbhyankar.SGA1.localDecompositionToGlobalIdealDecomposition
Documentation

A decomposition automorphism of the localized valuation ring stabilizes the original normalization prime.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
def localDecompositionToGlobalIdealDecomposition :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    decompositionGroup K (idealLocalizationValuationSubring B L P hP) →*
      HilbertRamification.Dedekind.decompositionGroup P Gal(L/K) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  let V := idealLocalizationValuationSubring B L P hP
  refine
    { toFun := fun tau ↦ ⟨(tau : Gal(L/K)), ?_⟩
      map_one' := rfl
      map_mul' := fun _ _ ↦ rfl }
  apply Ideal.ext
  intro b
  rw [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
  have hmap :
      idealLocalizationRingHom (B := B) (L := L) P hP
          ((tau : Gal(L/K))⁻¹ • b) =
        (tau⁻¹ : decompositionGroup K V) •
          idealLocalizationRingHom (B := B) (L := L) P hP b := by
    apply Subtype.ext
    exact algebraMap_normalization_smul (A := A)
      ((tau : Gal(L/K))⁻¹) b
  rw [← idealLocalizationRingHom_mem_maximalIdeal_iff (B := B) (L := L) P hP,
    hmap, ← idealLocalizationRingHom_mem_maximalIdeal_iff (B := B) (L := L) P hP]
  rw [IsLocalRing.mem_maximalIdeal, IsLocalRing.mem_maximalIdeal]
  exact not_congr
    (MulEquiv.isUnit_map
      (MulSemiringAction.toRingAut
        (decompositionGroup K V) V tau⁻¹))
def

idealDecompositionLocalizationMulEquiv

L223 ↗
TameAbhyankar.SGA1.idealDecompositionLocalizationMulEquiv
Documentation

The ideal decomposition group is canonically the decomposition group of the localized valuation subring.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
def idealDecompositionLocalizationMulEquiv :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    HilbertRamification.Dedekind.decompositionGroup P Gal(L/K) ≃*
      decompositionGroup K (idealLocalizationValuationSubring B L P hP) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  refine
    { toFun := globalIdealDecompositionToLocalDecomposition
        (A := A) (P := P) (hP := hP)
      invFun := localDecompositionToGlobalIdealDecomposition
        (A := A) (P := P) (hP := hP)
      left_inv := ?_
      right_inv := ?_
      map_mul' := fun _ _ ↦ rfl }
  · intro sigma
    apply Subtype.ext
    change (sigma : Gal(L/K)) = (sigma : Gal(L/K))
    rfl
  · intro tau
    apply Subtype.ext
    change (tau : Gal(L/K)) = (tau : Gal(L/K))
    rfl
theorem

idealLocalizationResidueEquiv_residueAction

L247 ↗
TameAbhyankar.SGA1.idealLocalizationResidueEquiv_residueAction
Documentation

Reduction commutes with the canonical comparison from ideal decomposition to valuation-subring decomposition.

Source context 19 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
Lean source · full declaration
theorem idealLocalizationResidueEquiv_residueAction
    [IsGalois K L] :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    letI := normalizationGaloisSMulCommClass
      (A := A) (B := B) (K := K) (L := L)
    ∀ (sigma : HilbertRamification.Dedekind.decompositionGroup P Gal(L/K))
      (x : B ⧸ P),
    let p := P.comap (algebraMap A B)
    letI : P.LiesOver p := ⟨rfl⟩
    idealLocalizationResidueEquiv B L P hP
        (HilbertRamification.Dedekind.residueStabilizerHom
          p P Gal(L/K) sigma x) =
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction
          K
          (idealLocalizationValuationSubring B L P hP)
          (globalIdealDecompositionToLocalDecomposition
            (A := A) (P := P) (hP := hP) sigma)
          (idealLocalizationResidueEquiv B L P hP x) := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  let := normalizationGaloisSMulCommClass
    (A := A) (B := B) (K := K) (L := L)
  intro sigma x
  let p := P.comap (algebraMap A B)
  let : P.LiesOver p := ⟨rfl⟩
  dsimp only
  refine Quotient.inductionOn x ?_
  intro b
  change
    idealLocalizationResidueEquiv B L P hP
        (HilbertRamification.Dedekind.residueStabilizerHom
          (P.comap (algebraMap A B)) P Gal(L/K) sigma
          (Ideal.Quotient.mk P b)) =
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction
          K (idealLocalizationValuationSubring B L P hP)
          (globalIdealDecompositionToLocalDecomposition
            (A := A) (P := P) (hP := hP) sigma)
          (idealLocalizationResidueEquiv B L P hP
            (Ideal.Quotient.mk P b))
  rw [HilbertRamification.Dedekind.residueStabilizerHom_apply,
    idealLocalizationResidueEquiv_mk,
    idealLocalizationResidueEquiv_mk,
    RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_residue]
  congr 1
  apply Subtype.ext
  exact algebraMap_normalization_smul (A := A) (sigma : Gal(L/K)) b
abbrev

normalizationIdealBasePrime

L298 ↗
TameAbhyankar.SGA1.normalizationIdealBasePrime
Documentation

The prime of the base ring below a normalization prime.

Source context 21 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
Lean source · statement
abbrev normalizationIdealBasePrime : Ideal A
theorem

normalizationIdealBasePrime_isMaximal

L303 ↗
TameAbhyankar.SGA1.normalizationIdealBasePrime_isMaximal
Source context 23 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
omit [IsFractionRing B L] [IsDedekindDomain B] in
Lean source · statement
theorem normalizationIdealBasePrime_isMaximal :
    (normalizationIdealBasePrime (A := A) P).IsMaximal
theorem

localDecomposition_fixes_normalizationBase

L312 ↗
TameAbhyankar.SGA1.localDecomposition_fixes_normalizationBase
Source context 23 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
omit [IsFractionRing A K] [IsIntegralClosure B A L]
  [Algebra.IsAlgebraic K L] [IsGalois K L] in
Lean source · statement
theorem localDecomposition_fixes_normalizationBase
    (sigma : decompositionGroup K
      (idealLocalizationValuationSubring B L P hP))
    (a : A) :
    sigma • idealLocalizationRingHom (B := B) (L := L) P hP
        (algebraMap A B a) =
      idealLocalizationRingHom (B := B) (L := L) P hP
        (algebraMap A B a)
def

normalizationBaseToDecompositionFixedSubring

L341 ↗
TameAbhyankar.SGA1.normalizationBaseToDecompositionFixedSubring
Documentation

The base ring maps canonically to the fixed valuation subring defining the intrinsic decomposition residue field.

Source context 22 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
Lean source · statement
def normalizationBaseToDecompositionFixedSubring :
    A →+* decompositionFixedSubring K
      (idealLocalizationValuationSubring B L P hP)
def

normalizationBaseResidueToDecompositionResidueField

L356 ↗
TameAbhyankar.SGA1.normalizationBaseResidueToDecompositionResidueField
Documentation

The canonical map from the base-prime residue field to the intrinsic decomposition residue field.

Source context 22 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
Lean source · statement
def normalizationBaseResidueToDecompositionResidueField :
    A ⧸ normalizationIdealBasePrime (A := A) P →+*
      decompositionResidueField K
        (idealLocalizationValuationSubring B L P hP)
theorem

normalizationBaseResidueToDecompositionResidueField_mk

L375 ↗
TameAbhyankar.SGA1.normalizationBaseResidueToDecompositionResidueField_mk
Source context 23 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
omit [IsFractionRing A K] [IsIntegralClosure B A L]
  [Algebra.IsAlgebraic K L] [IsGalois K L] in
Lean source · statement
theorem normalizationBaseResidueToDecompositionResidueField_mk
    (a : A) :
    normalizationBaseResidueToDecompositionResidueField
        (A := A) (P := P) (hP := hP)
        (Ideal.Quotient.mk (normalizationIdealBasePrime (A := A) P) a) =
      Ideal.Quotient.mk
        (decompositionFixedMaximalIdeal K
          (idealLocalizationValuationSubring B L P hP))
        (normalizationBaseToDecompositionFixedSubring
          (A := A) (B := B) (K := K) (L := L)
          (P := P) (hP := hP) a)
theorem

decompositionResidueField_algebraMap_mk

L389 ↗
TameAbhyankar.SGA1.decompositionResidueField_algebraMap_mk
Source context 23 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
omit [Algebra.IsAlgebraic K L] [IsGalois K L] in
Lean source · statement
theorem decompositionResidueField_algebraMap_mk
    (r : decompositionFixedSubring K
      (idealLocalizationValuationSubring B L P hP)) :
    algebraMap
        (decompositionResidueField K
          (idealLocalizationValuationSubring B L P hP))
        (selectedResidueField
          (idealLocalizationValuationSubring B L P hP))
        (Ideal.Quotient.mk
          (decompositionFixedMaximalIdeal K
            (idealLocalizationValuationSubring B L P hP)) r) =
      IsLocalRing.residue
        (idealLocalizationValuationSubring B L P hP) r
theorem

normalizationBaseResidue_decompositionResidueField_commutes

L408 ↗
TameAbhyankar.SGA1.normalizationBaseResidue_decompositionResidueField_commutes
Documentation

The canonical base-residue map agrees with the usual normalization residue map after localization.

Source context 23 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
omit [IsFractionRing A K] [IsIntegralClosure B A L]
  [Algebra.IsAlgebraic K L] [IsGalois K L] in
Lean source · full declaration
theorem normalizationBaseResidue_decompositionResidueField_commutes
    (x : A ⧸ normalizationIdealBasePrime (A := A) P) :
    letI : P.LiesOver (normalizationIdealBasePrime (A := A) P) := ⟨rfl⟩
    algebraMap
        (decompositionResidueField K
          (idealLocalizationValuationSubring B L P hP))
        (selectedResidueField
          (idealLocalizationValuationSubring B L P hP))
        (normalizationBaseResidueToDecompositionResidueField
          (A := A) (P := P) (hP := hP) x) =
      idealLocalizationResidueEquiv B L P hP
        (algebraMap
          (A ⧸ normalizationIdealBasePrime (A := A) P) (B ⧸ P) x) := by
  let : P.LiesOver (normalizationIdealBasePrime (A := A) P) := ⟨rfl⟩
  refine Quotient.inductionOn x ?_
  intro a
  change
    algebraMap
        (decompositionResidueField K
          (idealLocalizationValuationSubring B L P hP))
        (selectedResidueField
          (idealLocalizationValuationSubring B L P hP))
        (normalizationBaseResidueToDecompositionResidueField
          (A := A) (P := P) (hP := hP)
          (Ideal.Quotient.mk
            (normalizationIdealBasePrime (A := A) P) a)) =
      idealLocalizationResidueEquiv B L P hP
        (Ideal.Quotient.mk P (algebraMap A B a))
  rw [normalizationBaseResidueToDecompositionResidueField_mk,
    decompositionResidueField_algebraMap_mk,
    idealLocalizationResidueEquiv_mk]
  rfl
theorem

normalizationBaseResidueToDecompositionResidueField_surjective

L444 ↗
TameAbhyankar.SGA1.normalizationBaseResidueToDecompositionResidueField_surjective
Documentation

In residue characteristic zero, the canonical base-residue map onto the intrinsic decomposition residue field is surjective. The proof uses the normal residue extension and the naturality of the two residue actions.

Source context 22 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
Lean source · statement
theorem normalizationBaseResidueToDecompositionResidueField_surjective
    [FiniteDimensional K L]
    [IsIntegrallyClosed A]
    [CharZero (A ⧸ normalizationIdealBasePrime (A := A) P)] :
    Function.Surjective
      (normalizationBaseResidueToDecompositionResidueField
        (A := A) (B := B) (K := K) (L := L)
        (P := P) (hP := hP))
def

normalizationBaseResidueEquivDecompositionResidueField

L510 ↗
TameAbhyankar.SGA1.normalizationBaseResidueEquivDecompositionResidueField
Documentation

In residue characteristic zero, the residue field of the base prime is canonically the intrinsic decomposition residue field of the localized normalization.

Source context 22 commands

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

noncomputable section
universe uA uB uK uL
namespace TameAbhyankar.SGA1
open scoped Pointwise
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] Ideal.Quotient.field
section DecompositionLocalization
variable {A : Type uA} {B : Type uB} {K : Type uK} {L : Type uL}
variable [CommRing A] [CommRing B] [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra B L] [IsFractionRing B L]
variable [Algebra A B] [Algebra K L] [Algebra A L]
variable [IsScalarTower A K L] [IsScalarTower A B L]
variable [IsIntegralClosure B A L]
variable [Algebra.IsAlgebraic K L]
variable [IsDedekindDomain B]
variable (P : Ideal B) [P.IsMaximal]
variable (hP : P ≠ ⊥)
section BaseResidueField
variable [IsGalois K L]
include L
Lean source · statement
def normalizationBaseResidueEquivDecompositionResidueField
    [FiniteDimensional K L]
    [IsIntegrallyClosed A]
    [CharZero (A ⧸ normalizationIdealBasePrime (A := A) P)] :
    A ⧸ normalizationIdealBasePrime (A := A) P ≃+*
      decompositionResidueField K
        (idealLocalizationValuationSubring B L P hP)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.