NYLL
Module

ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
50 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists smul eq and card stabilizer eq ramification Idx mul inertia Deg

Imports38
  • Mathlib.Algebra.Module.Torsion.Free
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.Dimension.StrongRankCondition
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Integral
  • Mathlib.RingTheory.IntegralClosure.Algebra.Basic
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.DiscreteValuationRing.Basic
  • Mathlib.RingTheory.DedekindDomain.Basic
  • Mathlib.RingTheory.DedekindDomain.AdicValuation
  • Mathlib.RingTheory.DedekindDomain.Dvr
  • Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
  • Mathlib.NumberTheory.RamificationInertia.Ramification
  • Mathlib.RingTheory.RamificationInertia.Ramification
  • Mathlib.RingTheory.RamificationInertia.Inertia
  • Mathlib.Tactic.Ext
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.Algebra.GroupWithZero.Action.Defs
  • Mathlib.Algebra.Ring.Action.Field
  • Mathlib.Data.Set.Card
  • Mathlib.SetTheory.Cardinal.Finite
  • Mathlib.GroupTheory.GroupAction.Defs
  • Mathlib.GroupTheory.GroupAction.Quotient
  • Mathlib.FieldTheory.Galois.Basic
  • Mathlib.FieldTheory.Galois.IsGaloisGroup
  • Mathlib.RingTheory.DedekindDomain.IntegralClosure
  • Mathlib.RingTheory.Ideal.Pointwise
  • Mathlib.RingTheory.Invariant.Basic
  • Mathlib.RingTheory.Invariant.Galois
  • Mathlib.RingTheory.IsGaloisGroup.Basic
  • Mathlib.NumberTheory.RamificationInertia.Galois
  • Mathlib.RingTheory.Valuation.RamificationGroup
Imported by2

Declarations

theorem

isUnit_iff_inv_mem

L69 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.isUnit_iff_inv_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem isUnit_iff_inv_mem (V : ValuationSubring L) (x : V) (hx0 : (x : L) ≠ 0) :
    IsUnit x ↔ (x : L)⁻¹ ∈ V
theorem

mem_maximalIdeal_iff_inv_not_mem

L80 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.mem_maximalIdeal_iff_inv_not_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem mem_maximalIdeal_iff_inv_not_mem (V : ValuationSubring L) (x : V) (hx0 : (x : L) ≠ 0) :
    x ∈ maximalIdeal V ↔ (x : L)⁻¹ ∉ V
theorem

mem_nonunits_iff_eq_zero_or_inv_not_mem

L84 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.mem_nonunits_iff_eq_zero_or_inv_not_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem mem_nonunits_iff_eq_zero_or_inv_not_mem (V : ValuationSubring L) (x : L) :
    x ∈ V.nonunits ↔ x = 0 ∨ x⁻¹ ∉ V
theorem

inertiaDeg_maximalIdeal_eq_one_of_isLocalization

L100 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.inertiaDeg_maximalIdeal_eq_one_of_isLocalization
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem inertiaDeg_maximalIdeal_eq_one_of_isLocalization {R : Type*} [CommRing R]
    (p : Ideal R) [p.IsMaximal] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :
    (maximalIdeal Rₚ).inertiaDeg R = 1
structure

Over

L122 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.Over
Documentation

Compatibility of a valuation ring with a local base ring and its maximal ideal.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
Lean source · full declaration
structure Over (C : Type*) [CommRing C] [IsLocalRing C] {F : Type*} [Field F] [Algebra C F]
    (B : ValuationSubring F) : Prop where
  /-- The valuation ring contains the image of the local base ring. -/
  mem : ∀ c : C, algebraMap C F c ∈ B
  /-- The preimage of the valuation-ring nonunits is the maximal ideal of the base ring. -/
  nonunit_iff : ∀ c : C, algebraMap C F c ∈ B.nonunits ↔ c ∈ maximalIdeal C
abbrev

overAlgebra

L136 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.overAlgebra
Documentation

The algebra structure on the valuation subring induced by the base-ring map landing in it.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
abbrev overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) : Algebra C B
theorem

coe_algebraMap_overAlgebra

L139 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.coe_algebraMap_overAlgebra
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · full declaration
theorem coe_algebraMap_overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (c : C) :
    letI := overAlgebra B h
    ((algebraMap C B c : B) : F) = algebraMap C F c := rfl
theorem

isScalarTower_overAlgebra

L144 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.isScalarTower_overAlgebra
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · full declaration
theorem isScalarTower_overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    letI := overAlgebra B h
    IsScalarTower C B F := by
  let _ := overAlgebra B h
  exact IsScalarTower.of_algebraMap_eq fun a => rfl
theorem

algebraMap_injective

L151 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.algebraMap_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem algebraMap_injective : Function.Injective (algebraMap C F)
theorem

algebraMap_overAlgebra_injective

L156 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.algebraMap_overAlgebra_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · full declaration
theorem algebraMap_overAlgebra_injective (B : ValuationSubring F)
    (h : ∀ c : C, algebraMap C F c ∈ B) :
    letI := overAlgebra B h
    Function.Injective (algebraMap C B) := by
  let _ := overAlgebra B h
  intro a b hab
  have := congrArg (fun z : B => (z : F)) hab
  exact algebraMap_injective K this
theorem

comap_maximalIdeal_overAlgebra

L165 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.comap_maximalIdeal_overAlgebra
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · full declaration
theorem comap_maximalIdeal_overAlgebra (B : ValuationSubring F) (h : Over C B) :
    letI := overAlgebra B h.mem
    (maximalIdeal B).comap (algebraMap C B) = maximalIdeal C := by
  let _ := overAlgebra B h.mem
  ext c
  rw [Ideal.mem_comap, ← h.nonunit_iff, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl
theorem

liesOver_overAlgebra

L173 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.liesOver_overAlgebra
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · full declaration
theorem liesOver_overAlgebra (B : ValuationSubring F) (h : Over C B) :
    letI := overAlgebra B h.mem
    (maximalIdeal B).LiesOver (maximalIdeal C) := by
  let _ := overAlgebra B h.mem
  exact ⟨(comap_maximalIdeal_overAlgebra B h).symm⟩
theorem

mem_of_mem_integralClosure

L179 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.mem_of_mem_integralClosure
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem mem_of_mem_integralClosure (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    {y : F} (hy : y ∈ integralClosure C F) : y ∈ B
theorem

ne_top_of_over

L188 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.ne_top_of_over
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
Lean source · statement
theorem ne_top_of_over (B : ValuationSubring F) (h : Over C B) : B ≠ ⊤
theorem

maximalIdeal_ne_bot

L200 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.maximalIdeal_ne_bot
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
theorem maximalIdeal_ne_bot : maximalIdeal C ≠ ⊥
theorem

coe_algebraMap_integralClosure

L203 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.coe_algebraMap_integralClosure
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem coe_algebraMap_integralClosure (c : C) :
    ((algebraMap C (integralClosure C F) c : integralClosure C F) : F) = algebraMap C F c
theorem

algebraMap_integralClosure_injective

L207 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.algebraMap_integralClosure_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem algebraMap_integralClosure_injective :
    Function.Injective (algebraMap C (integralClosure C F))
theorem

isTorsionFree_integralClosure

L214 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.isTorsionFree_integralClosure
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
omit [IsDiscreteValuationRing C] in
Lean source · statement
theorem isTorsionFree_integralClosure : Module.IsTorsionFree C (integralClosure C F)
theorem

liesOver_maximalIdeal

L222 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.liesOver_maximalIdeal
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
theorem liesOver_maximalIdeal (v : HeightOneSpectrum (integralClosure C F)) :
    v.asIdeal.LiesOver (maximalIdeal C)
def

toOver

L230 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.toOver
Documentation

The inclusion of the integral closure into a valuation ring containing the base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def toOver (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    integralClosure C F →+* B
theorem

coe_toOver

L234 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.coe_toOver
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem coe_toOver (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (s : integralClosure C F) : ((toOver B h s : B) : F) = (s : F)
def

center

L238 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.center
Documentation

The center of the valuation on the integral closure of the local base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def center (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    Ideal (integralClosure C F)
theorem

mem_center_iff

L242 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.mem_center_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem mem_center_iff (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (s : integralClosure C F) :
    s ∈ center B h ↔ (s : F) ∈ B.nonunits
instance

center_isPrime

L248 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.center_isPrime
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
instance center_isPrime (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    (center B h).IsPrime
theorem

center_ne_bot

L253 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.center_ne_bot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
Lean source · statement
theorem center_ne_bot (B : ValuationSubring F) (h : Over C B) : center B h.mem ≠ ⊥
def

vOf

L264 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.vOf
Documentation

The height-one prime obtained from the center of a valuation lying over the local base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def vOf (B : ValuationSubring F) (h : Over C B) :
    HeightOneSpectrum (integralClosure C F)
theorem

isFractionRing_integralClosure

L274 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.isFractionRing_integralClosure
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
omit [IsDiscreteValuationRing C] [Algebra.IsSeparable K F] in
Lean source · statement
theorem isFractionRing_integralClosure : IsFractionRing (integralClosure C F) F
theorem

isDedekindDomain_integralClosure

L277 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.isDedekindDomain_integralClosure
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
Lean source · statement
theorem isDedekindDomain_integralClosure : IsDedekindDomain (integralClosure C F)
theorem

finite_integralClosure

L280 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.finite_integralClosure
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
Lean source · statement
theorem finite_integralClosure : Module.Finite C (integralClosure C F)
def

W

L284 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.W
Documentation

The valuation ring at a height-one prime of the Dedekind integral closure.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
Lean source · statement
def W (v : HeightOneSpectrum (integralClosure C F)) : ValuationSubring F
theorem

W_def

L289 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.W_def
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
Lean source · full declaration
theorem W_def (v : HeightOneSpectrum (integralClosure C F)) :
    letI := isFractionRing_integralClosure K (F := F) (C := C)
    letI := isDedekindDomain_integralClosure K (F := F) (C := C)
    W K v = HeightOneSpectrum.valuationSubringAtPrime F v := rfl
abbrev

Wv

L313 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.Wv
Documentation

The valuation ring of a height-one prime of the integral closure.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
Lean source · statement
abbrev Wv (v : HeightOneSpectrum (integralClosure C F)) : ValuationSubring F
theorem

coe_algebraMap_Wv

L316 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.coe_algebraMap_Wv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem coe_algebraMap_Wv (v : HeightOneSpectrum (integralClosure C F)) (s : integralClosure C F) :
    ((algebraMap (integralClosure C F) (Wv v) s : Wv v) : F) = (s : F)
theorem

over_Wv

L319 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.over_Wv
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
Lean source · statement
theorem over_Wv (v : HeightOneSpectrum (integralClosure C F)) : Over C (Wv v)
theorem

Wv_vOf_le

L331 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.Wv_vOf_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
Lean source · statement
theorem Wv_vOf_le (B : ValuationSubring F) (h : Over C B) : Wv (vOf K B h) ≤ B
theorem

Wv_vOf_eq

L344 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.Wv_vOf_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
Lean source · statement
theorem Wv_vOf_eq (B : ValuationSubring F) (h : Over C B) : Wv (vOf K B h) = B
theorem

vOf_Wv

L347 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.vOf_Wv
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
Lean source · statement
theorem vOf_Wv (v : HeightOneSpectrum (integralClosure C F)) : vOf K (Wv v) (over_Wv v) = v
theorem

ramificationIdx_mul_inertiaDeg_Wv

L354 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.ramificationIdx_mul_inertiaDeg_Wv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section dict2
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [IsFractionRing (integralClosure C F) F] [IsDedekindDomain (integralClosure C F)]
include K in
Lean source · full declaration
theorem ramificationIdx_mul_inertiaDeg_Wv (v : HeightOneSpectrum (integralClosure C F))
    (hv : ∀ c : C, algebraMap C F c ∈ Wv v) :
    letI := overAlgebra (Wv v) hv
    (maximalIdeal C).ramificationIdx' (maximalIdeal (Wv v)) *
      (maximalIdeal (Wv v)).inertiaDeg C =
    (maximalIdeal C).ramificationIdx' v.asIdeal * v.asIdeal.inertiaDeg C := by
  let _ : Algebra C (Wv v) := overAlgebra (Wv v) hv
  have _ := liesOver_maximalIdeal v
  have _ : IsScalarTower C (integralClosure C F) (Wv v) :=
    IsScalarTower.of_algebraMap_eq fun a => Subtype.ext rfl
  have _ : IsDiscreteValuationRing (Wv v) :=
    IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain (integralClosure C F)
      v.ne_bot (Wv v)
  have hmapS : Ideal.map (algebraMap (integralClosure C F) (Wv v)) v.asIdeal =
      maximalIdeal (Wv v) :=
    IsLocalization.AtPrime.map_eq_maximalIdeal v.asIdeal (Wv v)
  have hmW0 : maximalIdeal (Wv v) ≠ ⊥ := IsDiscreteValuationRing.not_a_field _
  have : (maximalIdeal (Wv v)).LiesOver v.asIdeal :=
    ⟨(IsLocalization.AtPrime.under_maximalIdeal (Wv v) v.asIdeal).symm⟩
  have he : (maximalIdeal C).ramificationIdx' (maximalIdeal (Wv v)) =
      (maximalIdeal C).ramificationIdx' v.asIdeal *
        v.asIdeal.ramificationIdx' (maximalIdeal (Wv v)) :=
    Ideal.ramificationIdx'_algebra_tower (by rw [hmapS]; exact hmW0)
      (by
        rw [Ne, Ideal.map_eq_bot_iff_of_injective (algebraMap_overAlgebra_injective K _ _)]
        exact maximalIdeal_ne_bot)
      hmapS.le
  have he1 : v.asIdeal.ramificationIdx' (maximalIdeal (Wv v)) = 1 := by
    rw [← hmapS]
    exact Ideal.ramificationIdx'_map_self_eq_one
      (by rw [hmapS]; exact (maximalIdeal.isMaximal _).ne_top) (by rw [hmapS]; exact hmW0)
  have hf : (maximalIdeal (Wv v)).inertiaDeg C =
      v.asIdeal.inertiaDeg C * (maximalIdeal (Wv v)).inertiaDeg (integralClosure C F) :=
    Ideal.inertiaDeg_tower _ _
  have hf1 : (maximalIdeal (Wv v)).inertiaDeg (integralClosure C F) = 1 :=
    inertiaDeg_maximalIdeal_eq_one_of_isLocalization v.asIdeal (Wv v)
  rw [he, he1, hf, hf1, mul_one, mul_one]
theorem

smul_algebraMap

L407 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.smul_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
omit [IsDomain C] [IsDiscreteValuationRing C] [IsFractionRing C K]
    [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
    [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
    [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M] in
Lean source · statement
theorem smul_algebraMap (σ : M ≃ₐ[K] M) (c : C) : σ • algebraMap C M c = algebraMap C M c
theorem

mem_smul_nonunits_iff

L410 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.mem_smul_nonunits_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
Lean source · statement
theorem mem_smul_nonunits_iff (σ : M ≃ₐ[K] M) (V : ValuationSubring M) (x : M) :
    x ∈ (σ • V).nonunits ↔ σ⁻¹ • x ∈ V.nonunits
theorem

over_smul

L418 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.over_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
omit [IsFractionRing C K] [IsFractionRing (integralClosure C M) M]
    [IsDedekindDomain (integralClosure C M)]
    [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
    [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M] in
Lean source · statement
theorem over_smul (V : ValuationSubring M) (h : Over C V) (σ : M ≃ₐ[K] M) : Over C (σ • V)
theorem

coe_smul_integralClosure

L425 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.coe_smul_integralClosure
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
omit [IsDomain C] [IsDiscreteValuationRing C] [Algebra C K] [IsFractionRing C K]
    [IsScalarTower C K M] [IsFractionRing (integralClosure C M) M]
    [IsDedekindDomain (integralClosure C M)] in
Lean source · statement
theorem coe_smul_integralClosure (σ : M ≃ₐ[K] M) (s : integralClosure C M) :
    ((σ • s : integralClosure C M) : M) = σ • (s : M)
theorem

center_smul

L433 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.center_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
omit [IsDomain C] [IsDiscreteValuationRing C] [Algebra C K] [IsFractionRing C K] [IsScalarTower C K
  M]
    [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)] in
Lean source · statement
theorem center_smul (V : ValuationSubring M) (h : ∀ c : C, algebraMap C M c ∈ V) (σ : M ≃ₐ[K] M)
    (h' : ∀ c : C, algebraMap C M c ∈ σ • V) :
    center (σ • V) h' = σ • center V h
theorem

center_congr

L441 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.center_congr
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
omit [IsDomain C] [IsDiscreteValuationRing C]
    [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)] in
Lean source · statement
theorem center_congr (V₁ V₂ : ValuationSubring M) (h₁ : ∀ c : C, algebraMap C M c ∈ V₁)
    (h₂ : ∀ c : C, algebraMap C M c ∈ V₂) (hV : V₁ = V₂) : center V₁ h₁ = center V₂ h₂
theorem

exists_smul_eq

L448 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.exists_smul_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
variable [FiniteDimensional K M] [IsGaloisGroup (M ≃ₐ[K] M) C (integralClosure C M)]
include K in
Lean source · statement
theorem exists_smul_eq (V V' : ValuationSubring M) (h : Over C V) (h' : Over C V') :
    ∃ σ : M ≃ₐ[K] M, σ • V' = V
theorem

stabilizer_eq

L461 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.stabilizer_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
variable [FiniteDimensional K M] [IsGaloisGroup (M ≃ₐ[K] M) C (integralClosure C M)]
omit [FiniteDimensional K M] [IsGaloisGroup (M ≃ₐ[K] M) C (integralClosure C M)] in
Lean source · statement
theorem stabilizer_eq (V : ValuationSubring M) (h : Over C V) :
    MulAction.stabilizer (M ≃ₐ[K] M) V =
      MulAction.stabilizer (M ≃ₐ[K] M) (center V h.mem)
theorem

card_stabilizer

L480 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.card_stabilizer
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section galois
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [IsFractionRing (integralClosure C M) M] [IsDedekindDomain (integralClosure C M)]
variable [MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M)]
variable [SMulDistribClass (M ≃ₐ[K] M) (integralClosure C M) M]
variable [FiniteDimensional K M] [IsGaloisGroup (M ≃ₐ[K] M) C (integralClosure C M)]
variable [Module.Finite C (integralClosure C M)]
include K in
Lean source · statement
theorem card_stabilizer (V : ValuationSubring M) (h : Over C V) :
    Nat.card ↥(MulAction.stabilizer (M ≃ₐ[K] M) V) =
      (maximalIdeal C).ramificationIdx' (vOf K V h).asIdeal *
        (vOf K V h).asIdeal.inertiaDeg C
theorem

ef_congr

L516 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.ef_congr
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section assembly
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [FiniteDimensional K M] [IsGalois K M]
Lean source · full declaration
theorem ef_congr (V₁ V₂ : ValuationSubring M) (h₁ : ∀ c : C, algebraMap C M c ∈ V₁)
    (h₂ : ∀ c : C, algebraMap C M c ∈ V₂) (hV : V₁ = V₂) :
    (letI := overAlgebra V₁ h₁
     (maximalIdeal C).ramificationIdx' (maximalIdeal V₁) * (maximalIdeal V₁).inertiaDeg C) =
    (letI := overAlgebra V₂ h₂
     (maximalIdeal C).ramificationIdx' (maximalIdeal V₂) * (maximalIdeal V₂).inertiaDeg C) := by
  subst hV; rfl
theorem

main

L524 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg.EmbCountGal.main
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
namespace EmbCountGal
open IsLocalRing IsDedekindDomain
open scoped Pointwise
section assembly
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
variable [FiniteDimensional K M] [IsGalois K M]
include K in
Lean source · full declaration
theorem main (V : ValuationSubring M) (hCV : ∀ c : C, algebraMap C M c ∈ V)
    (hCVmax : ∀ c : C, algebraMap C M c ∈ V.nonunits ↔ c ∈ maximalIdeal C) :
    (∀ V' : ValuationSubring M, (∀ c : C, algebraMap C M c ∈ V') →
        (∀ c : C, algebraMap C M c ∈ V'.nonunits ↔ c ∈ maximalIdeal C) →
        ∃ g : M ≃ₐ[K] M, g • V' = V) ∧
    Nat.card ↥(V.decompositionSubgroup K) =
      (letI : Algebra C ↥V := ((algebraMap C M).codRestrict V hCV).toAlgebra
       (maximalIdeal C).ramificationIdx' (maximalIdeal ↥V) *
         (maximalIdeal ↥V).inertiaDeg C) := by
  have _ := isFractionRing_integralClosure K (F := M) (C := C)
  have _ := isDedekindDomain_integralClosure K (F := M) (C := C)
  have _ := finite_integralClosure K (F := M) (C := C)
  let _ : MulSemiringAction (M ≃ₐ[K] M) (integralClosure C M) :=
    IsIntegralClosure.MulSemiringAction C K M (integralClosure C M)
  have _ : IsGaloisGroup (M ≃ₐ[K] M) C (integralClosure C M) :=
    IsGaloisGroup.of_isFractionRing _ _ _ K M
  have h : Over C V := ⟨hCV, hCVmax⟩
  refine ⟨fun V' h1 h2 => exists_smul_eq K V V' h ⟨h1, h2⟩, ?_⟩
  change Nat.card ↥(MulAction.stabilizer (M ≃ₐ[K] M) V) = _
  rw [card_stabilizer K V h]
  have hv : ∀ c : C, algebraMap C M c ∈ Wv (vOf K V h) := (over_Wv (vOf K V h)).mem
  rw [← ramificationIdx_mul_inertiaDeg_Wv K (vOf K V h) hv]
  exact ef_congr _ _ _ _ (Wv_vOf_eq K V h)
theorem

exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg

L554 ↗
ValuationSubring.exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing in
open scoped Pointwise in
Lean source · full declaration
theorem _root_.ValuationSubring.exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg
    {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
    (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
    {M : Type*} [Field M] [Algebra K M] [Algebra C M] [IsScalarTower C K M]
    [FiniteDimensional K M] [IsGalois K M]
    (V : ValuationSubring M) (hCV : ∀ c : C, algebraMap C M c ∈ V)
    (hCVmax : ∀ c : C, algebraMap C M c ∈ V.nonunits ↔ c ∈ maximalIdeal C) :
    (∀ V' : ValuationSubring M, (∀ c : C, algebraMap C M c ∈ V') →
        (∀ c : C, algebraMap C M c ∈ V'.nonunits ↔ c ∈ maximalIdeal C) →
        ∃ g : M ≃ₐ[K] M, g • V' = V) ∧
    Nat.card ↥(V.decompositionSubgroup K) =
      (letI : Algebra C ↥V := ((algebraMap C M).codRestrict V hCV).toAlgebra
       (maximalIdeal C).ramificationIdx' (maximalIdeal ↥V) *
         (maximalIdeal ↥V).inertiaDeg C) :=
  EmbCountGal.main K V hCV hCVmax

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