Module

ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg

50 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring nat Card alg Hom comap eq ramification Idx mul inertia Deg

Imports78

Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Algebra.Hom
Mathlib.Algebra.Algebra.Subalgebra.Basic
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Defs
Mathlib.Algebra.BigOperators.Ring.Finset
Mathlib.Algebra.Group.Action.Defs
Mathlib.Algebra.Group.DivInvMonoid
Mathlib.Algebra.Group.Equiv.Basic
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Group.Units.Defs
Mathlib.Algebra.GroupWithZero.Units.Lemmas
Mathlib.Algebra.Module.Torsion.Free
Mathlib.Algebra.Prime.Defs
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Algebra.Ring.Subsemiring.Basic
Mathlib.Data.Finset.Defs
Mathlib.Data.Fintype.Card
Mathlib.Data.Set.Card
Mathlib.Data.Set.Finite.Basic
Mathlib.Data.SetLike.Basic
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Galois.IsGaloisGroup
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.Normal.Closure
Mathlib.FieldTheory.Normal.Defs
Mathlib.FieldTheory.Separable
Mathlib.FieldTheory.SeparableClosure
Mathlib.GroupTheory.GroupAction.Defs
Mathlib.GroupTheory.Index
Mathlib.LinearAlgebra.Dimension.Finite
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.Localization
Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.Logic.Equiv.Basic
Mathlib.Logic.Equiv.Set
Mathlib.NumberTheory.RamificationInertia.Galois
Mathlib.NumberTheory.RamificationInertia.Ramification
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.DedekindDomain.Basic
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Nonunits
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Pointwise
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.Invariant.Basic
Mathlib.RingTheory.Invariant.Galois
Mathlib.RingTheory.IsGaloisGroup.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.RamificationInertia.Basic
Mathlib.RingTheory.RamificationInertia.Inertia
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.RingTheory.SimpleRing.Basic
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

isUnit_iff_inv_mem

L111 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.isUnit_iff_inv_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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 isUnit_iff_inv_mem {L : Type*} [Field L] (B : ValuationSubring L) (x : B)
    (hx0 : (x : L) ≠ 0) : IsUnit x ↔ (x : L)⁻¹ ∈ B

theorem

mem_maximalIdeal_iff_inv_not_mem

L122 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.mem_maximalIdeal_iff_inv_not_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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 mem_maximalIdeal_iff_inv_not_mem {L : Type*} [Field L] (B : ValuationSubring L) (x : B)
    (hx0 : (x : L) ≠ 0) : x ∈ maximalIdeal B ↔ (x : L)⁻¹ ∉ B

theorem

mem_nonunits_iff_eq_zero_or

L126 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.mem_nonunits_iff_eq_zero_or

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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 mem_nonunits_iff_eq_zero_or {L : Type*} [Field L] (B : ValuationSubring L) (x : L) :
    x ∈ B.nonunits ↔ x ∈ B ∧ (x = 0 ∨ x⁻¹ ∉ B)

theorem

mem_nonunits_comap_iff

L147 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.mem_nonunits_comap_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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 mem_nonunits_comap_iff {L L' : Type*} [Field L] [Field L'] (B : ValuationSubring L')
    (f : L →+* L') (x : L) : x ∈ (B.comap f).nonunits ↔ f x ∈ B.nonunits

theorem

inertiaDeg_maximalIdeal_eq_one_of_isLocalization

L152 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.inertiaDeg_maximalIdeal_eq_one_of_isLocalization

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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 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

def

Over

L174 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.Over

Documentation

The condition that the base ring maps into the valuation ring with the same nonunits.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit K in

Lean source · statement

def Over (B : ValuationSubring F) : Prop

abbrev

overAlgebra

L178 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.overAlgebra

Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in

Lean source · statement

abbrev overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) : Algebra C B

theorem

coe_algebraMap_overAlgebra

L181 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.coe_algebraMap_overAlgebra

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit K [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

L186 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.isScalarTower_overAlgebra

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit K [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

L193 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.algebraMap_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K in

Lean source · statement

theorem algebraMap_injective : Function.Injective (algebraMap C F)

theorem

algebraMap_overAlgebra_injective

L198 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.algebraMap_overAlgebra_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K 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 h' : algebraMap C F a = algebraMap C F b := congrArg (fun z : B => (z : F)) hab
  exact algebraMap_injective (C := C) K h'

theorem

comap_maximalIdeal_overAlgebra

L207 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.comap_maximalIdeal_overAlgebra

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit K in

Lean source · full declaration

theorem comap_maximalIdeal_overAlgebra (B : ValuationSubring F) (h : Over C B) :
    letI := overAlgebra B h.1
    (maximalIdeal B).comap (algebraMap C B) = maximalIdeal C := by
  let := overAlgebra B h.1
  ext c
  rw [Ideal.mem_comap, ← h.2 c, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl

theorem

mem_of_mem_integralClosure

L215 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.mem_of_mem_integralClosure

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
omit K [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

maximalIdeal_ne_bot

L226 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.maximalIdeal_ne_bot

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
omit K in

Lean source · statement

theorem maximalIdeal_ne_bot : maximalIdeal C ≠ ⊥

theorem

ne_top_of_over

L229 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.ne_top_of_over

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
include K in

Lean source · statement

theorem ne_top_of_over (B : ValuationSubring F) (h : Over C B) : B ≠ ⊤

theorem

coe_algebraMap_integralClosure

L239 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.coe_algebraMap_integralClosure

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
omit K [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

L243 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.algebraMap_integralClosure_injective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K in

Lean source · statement

theorem algebraMap_integralClosure_injective :
    Function.Injective (algebraMap C (integralClosure C F))

theorem

isTorsionFree_integralClosure

L251 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.isTorsionFree_integralClosure

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
omit [IsDiscreteValuationRing C] in
include K in

Lean source · statement

theorem isTorsionFree_integralClosure : Module.IsTorsionFree C (integralClosure C F)

theorem

liesOver_maximalIdeal

L259 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.liesOver_maximalIdeal

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in

Lean source · statement

theorem liesOver_maximalIdeal (v : HeightOneSpectrum (integralClosure C F)) :
    v.asIdeal.LiesOver (maximalIdeal C)

def

toOver

L269 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.toOver

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal

Lean source · statement

def toOver (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    integralClosure C F →+* B

theorem

coe_toOver

L273 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.coe_toOver

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
omit K [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

L277 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.center

Documentation

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

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal

Lean source · statement

def center (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    Ideal (integralClosure C F)

theorem

mem_center_iff

L281 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.mem_center_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
omit K [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

L286 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.center_isPrime

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal

Lean source · statement

instance center_isPrime (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    (center B h).IsPrime

theorem

comap_center

L291 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.comap_center

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
omit K in

Lean source · statement

theorem comap_center (B : ValuationSubring F) (h : Over C B) :
    (center B h.1).comap (algebraMap C (integralClosure C F)) = maximalIdeal C

instance

center_liesOver

L296 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.center_liesOver

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal

Lean source · statement

instance center_liesOver (B : ValuationSubring F) (h : Over C B) :
    (center B h.1).LiesOver (maximalIdeal C)

theorem

center_ne_bot

L301 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.center_ne_bot

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
include K in

Lean source · statement

theorem center_ne_bot (B : ValuationSubring F) (h : Over C B) : center B h.1 ≠ ⊥

def

vOf

L310 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.vOf

Documentation

The height-one prime defined by the center of a valuation above the local base ring.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
include K in

Lean source · statement

def vOf (B : ValuationSubring F) (h : Over C B) :
    HeightOneSpectrum (integralClosure C F)

theorem

vOf_asIdeal

L314 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.vOf_asIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal

Lean source · statement

theorem vOf_asIdeal (B : ValuationSubring F) (h : Over C B) :
    (vOf K B h).asIdeal = center B h.1

abbrev

W

L322 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.W

Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]

Lean source · statement

abbrev W (v : HeightOneSpectrum (integralClosure C F)) : ValuationSubring F

theorem

isDiscreteValuationRing_W

L325 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.isDiscreteValuationRing_W

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
omit [IsDomain C] [IsDiscreteValuationRing C] in

Lean source · statement

theorem isDiscreteValuationRing_W (v : HeightOneSpectrum (integralClosure C F)) :
    IsDiscreteValuationRing (W v)

theorem

coe_algebraMap_W

L330 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.coe_algebraMap_W

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
omit K [IsDomain C] [IsDiscreteValuationRing C] in

Lean source · statement

theorem coe_algebraMap_W (v : HeightOneSpectrum (integralClosure C F)) (s : integralClosure C F) :
    ((algebraMap (integralClosure C F) (W v) s : W v) : F) = (s : F)

theorem

over_W

L333 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.over_W

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
omit K in

Lean source · statement

theorem over_W (v : HeightOneSpectrum (integralClosure C F)) : Over C (W v)

theorem

W_vOf_le

L343 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.W_vOf_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]

Lean source · statement

theorem W_vOf_le (B : ValuationSubring F) (h : Over C B) : W (vOf K B h) ≤ B

theorem

W_vOf_eq

L356 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.W_vOf_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]

Lean source · statement

theorem W_vOf_eq (B : ValuationSubring F) (h : Over C B) : W (vOf K B h) = B

theorem

vOf_W

L359 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.vOf_W

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]

Lean source · statement

theorem vOf_W (v : HeightOneSpectrum (integralClosure C F)) : vOf K (W v) (over_W v) = v

theorem

eq_of_center_eq

L366 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.eq_of_center_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
include K in

Lean source · statement

theorem eq_of_center_eq (B B' : ValuationSubring F) (h : Over C B) (h' : Over C B')
    (hc : center B h.1 = center B' h'.1) : B = B'

def

ef

L373 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.ef

Documentation

The product of the ramification index and residue degree above the base maximal ideal.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]

Lean source · statement

def ef (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) : ℕ

theorem

ef_W

L377 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.ef_W

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
include K in

Lean source · statement

theorem ef_W (v : HeightOneSpectrum (integralClosure C F)) :
    ef (W v) (over_W v).1 =
    (maximalIdeal C).ramificationIdx' v.asIdeal * v.asIdeal.inertiaDeg C

theorem

ef_eq

L411 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.ef_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
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]
variable (C) in
variable (C) in
attribute [local instance] liesOver_maximalIdeal
section dedekind
variable [IsDedekindDomain (integralClosure C F)] [IsFractionRing (integralClosure C F) F]
include K in

Lean source · statement

theorem ef_eq (B : ValuationSubring F) (h : Over C B) :
    ef B h.1 = (maximalIdeal C).ramificationIdx' (center B h.1) *
      (center B h.1).inertiaDeg C

def

jS

L436 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.jS

Documentation

The map between integral closures induced by the inclusion of the intermediate field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]

Lean source · statement

def jS : integralClosure C κ →ₐ[C] integralClosure C N

theorem

coe_jS

L441 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.coe_jS

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]
omit K [IsDomain C] [IsDiscreteValuationRing C] in

Lean source · statement

theorem coe_jS (s : integralClosure C κ) :
    ((jS (C := C) (κ := κ) (N := N) s : integralClosure C N) : N) = algebraMap κ N s

theorem

jS_injective

L444 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.jS_injective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]
omit K [IsDomain C] [IsDiscreteValuationRing C] in

Lean source · statement

theorem jS_injective : Function.Injective (jS (C := C) (κ := κ) (N := N))

theorem

card_smul_mem

L449 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.card_smul_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]

Lean source · statement

theorem card_smul_mem {G X : Type*} [Group G] [MulAction G X] [Finite G] (x₀ : X) (T : Set X)
    (hT : T ⊆ MulAction.orbit G x₀) (hTfin : T.Finite) :
    Nat.card {g : G // g • x₀ ∈ T} = Nat.card T * Nat.card (MulAction.stabilizer G x₀)

theorem

over_comap

L470 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.over_comap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]
omit N [IsFractionRing C K] in

Lean source · statement

theorem over_comap {N' : Type*} [Field N'] [Algebra K N'] [Algebra C N'] [IsScalarTower C K N']
    (V : ValuationSubring N') (hV : Over C V) (τ : κ →ₐ[K] N') :
    Over C (V.comap (τ : κ →+* N'))

def

twist

L482 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.twist

Documentation

The intermediate-field embedding obtained by composing inclusion with an automorphism.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]

Lean source · statement

def twist (g : N ≃ₐ[K] N) : κ →ₐ[K] N

theorem

twist_apply

L485 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.twist_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]
omit C in

Lean source · statement

theorem twist_apply (g : N ≃ₐ[K] N) (x : κ) :
    twist K (κ := κ) g x = g (algebraMap κ N x)

theorem

card_twist

L492 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.card_twist

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Gal
open scoped Pointwise
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {κ : Type*} [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ]
variable {N : Type*} [Field N] [Algebra K N] [Algebra C N] [IsScalarTower C K N]
variable [Algebra κ N] [IsScalarTower K κ N] [IsScalarTower C κ N]
variable [FiniteDimensional K N] [IsGalois K N]
variable [IsDedekindDomain (integralClosure C κ)] [IsFractionRing (integralClosure C κ) κ]
variable [IsDedekindDomain (integralClosure C N)] [IsFractionRing (integralClosure C N) N]

Lean source · statement

theorem card_twist (V : ValuationSubring N) (hV : Over C V) (B : ValuationSubring κ)
    (hB : Over C B) [FiniteDimensional K κ] [Algebra.IsSeparable K κ] :
    Nat.card {g : N ≃ₐ[K] N // V.comap (twist K (κ := κ) g : κ →+* N) = B} =
      Module.finrank κ N * ef B hB.1

theorem

card_stabilizer_algHom

L676 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg.KFA2a.card_stabilizer_algHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace KFA2a
section Emb
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]

Lean source · statement

theorem card_stabilizer_algHom {κ N : Type*} [Field κ] [Field N] [Algebra K κ] [Algebra K N]
    [Algebra κ N] [IsScalarTower K κ N] [FiniteDimensional K N] [IsGalois K N]
    (act : MulAction (N ≃ₐ[K] N) (κ →ₐ[K] N))
    (hact : ∀ (g : N ≃ₐ[K] N) (τ : κ →ₐ[K] N), g • τ = (g : N →ₐ[K] N).comp τ) :
    Nat.card (MulAction.stabilizer (N ≃ₐ[K] N) (IsScalarTower.toAlgHom K κ N)) =
      Module.finrank κ N

theorem

natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg

L702 ↗

ValuationSubring.natCard_algHom_comap_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_natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
open KFA2a in

Lean source · full declaration

theorem _root_.ValuationSubring.natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg
    {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
    (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
    {L : Type*} [Field L] [IsAlgClosed L] [Algebra C L] [Algebra K L] [IsScalarTower C K L]
      [Algebra.IsAlgebraic K L]
    (A : ValuationSubring L) (hCA : ∀ c : C, algebraMap C L c ∈ A)
    (hCAmax : ∀ c : C, (⟨algebraMap C L c, hCA c⟩ : ↥A) ∈ maximalIdeal ↥A ↔ c ∈ maximalIdeal C)
    (κ : Type*) [Field κ] [Algebra K κ] [Algebra C κ] [IsScalarTower C K κ] [FiniteDimensional K κ]
      [Algebra.IsSeparable K κ]
    (B : ValuationSubring κ) (hCB : ∀ c : C, algebraMap C κ c ∈ B)
    (hCBmax : ∀ c : C, (⟨algebraMap C κ c, hCB c⟩ : ↥B) ∈ maximalIdeal ↥B ↔ c ∈ maximalIdeal C) :
    Finite {σ : κ →ₐ[K] L // A.comap (σ : κ →+* L) = B} ∧
    Nat.card {σ : κ →ₐ[K] L // A.comap (σ : κ →+* L) = B} =
      (letI : Algebra C ↥B := ((algebraMap C κ).codRestrict B hCB).toAlgebra
       (maximalIdeal C).ramificationIdx' (maximalIdeal ↥B) * (maximalIdeal ↥B).inertiaDeg C) := by
  classical
  refine ⟨inferInstance, ?_⟩
  have hB : KFA2a.Over C B :=
    ⟨hCB, fun c => by rw [← hCBmax c, ← ValuationSubring.coe_mem_nonunits_iff]⟩
  have hA : KFA2a.Over C A :=
    ⟨hCA, fun c => by rw [← hCAmax c, ← ValuationSubring.coe_mem_nonunits_iff]⟩
  have : IsAlgClosure K L := (isAlgClosure_iff K L).mpr ⟨inferInstance, inferInstance⟩
  set N : IntermediateField K L := IntermediateField.normalClosure K κ L with hN
  have : Algebra.IsSeparable K N := by
    rw [hN, normalClosure_def]
    have : ∀ f : κ →ₐ[K] L, Algebra.IsSeparable K f.fieldRange := fun f =>
      ⟨fun x => by
        obtain ⟨y, hy⟩ := (AlgHom.mem_fieldRange).mp x.2
        refine IsSeparable.of_algHom (F := K) (K := ↥f.fieldRange) (E := L)
          (f := f.fieldRange.val) ?_
        change IsSeparable K (x : L)
        rw [← hy]
        exact IsSeparable.map f f.injective (Algebra.IsSeparable.isSeparable K y)⟩
    infer_instance
  have : IsGalois K N := IsGalois.mk
  have hne : Nonempty (κ →ₐ[K] L) := ⟨IsAlgClosed.lift⟩
  let σ₀ : κ →ₐ[K] N := (normalClosure.algHomEquiv K κ L).symm hne.some
  let : Algebra κ N := σ₀.toRingHom.toAlgebra
  have : IsScalarTower K κ N := IsScalarTower.of_algebraMap_eq (fun x => (σ₀.commutes x).symm)
  have : IsScalarTower C κ N := IsScalarTower.of_algebraMap_eq (fun c => by
    change algebraMap C N c = σ₀ (algebraMap C κ c)
    rw [IsScalarTower.algebraMap_apply C K κ, AlgHom.commutes, ← IsScalarTower.algebraMap_apply])
  have hσ₀ : IsScalarTower.toAlgHom K κ N = σ₀ := AlgHom.ext fun x => rfl
  have : IsFractionRing (integralClosure C κ) κ :=
    integralClosure.isFractionRing_of_finite_extension K κ
  have : IsDedekindDomain (integralClosure C κ) :=
    IsIntegralClosure.isDedekindDomain C K κ (integralClosure C κ)
  have : IsFractionRing (integralClosure C N) N :=
    integralClosure.isFractionRing_of_finite_extension K N
  have : IsDedekindDomain (integralClosure C N) :=
    IsIntegralClosure.isDedekindDomain C K N (integralClosure C N)
  let ι : N →ₐ[K] L := N.val
  have hAN : KFA2a.Over C (A.comap (ι : N →+* L)) := KFA2a.over_comap K A hA ι
  have hcount := KFA2a.card_twist K (A.comap (ι : N →+* L)) hAN B hB
  let act : MulAction (N ≃ₐ[K] N) (κ →ₐ[K] N) :=
    { smul := fun g τ => (g : N →ₐ[K] N).comp τ
      one_smul := fun τ => by ext; rfl
      mul_smul := fun g h τ => by ext; rfl }
  have hact : ∀ (g : N ≃ₐ[K] N) (τ : κ →ₐ[K] N), g • τ = (g : N →ₐ[K] N).comp τ := fun _ _ => rfl
  have htwist : ∀ g : N ≃ₐ[K] N, KFA2a.twist K (κ := κ) g = g • IsScalarTower.toAlgHom K κ N :=
    fun g => rfl
  have horbit : ∀ τ : κ →ₐ[K] N, τ ∈ MulAction.orbit (N ≃ₐ[K] N) (IsScalarTower.toAlgHom K κ N) :=
    by
    intro τ
    let φ : N →ₐ[K] N := AlgHom.liftNormal τ N
    have hφ : ∀ x : κ, φ (algebraMap κ N x) = τ x := fun x => AlgHom.liftNormal_commutes τ N x
    refine MulAction.mem_orbit_iff.mpr ⟨AlgEquiv.ofBijective φ (AlgHom.normal_bijective K N N φ),
      ?_⟩
    rw [hact]
    exact AlgHom.ext fun x => hφ x
  set T : Set (κ →ₐ[K] N) := {τ | (A.comap (ι : N →+* L)).comap (τ : κ →+* N) = B} with hT
  have h1 : Nat.card {g : N ≃ₐ[K] N //
      (A.comap (ι : N →+* L)).comap (KFA2a.twist K (κ := κ) g : κ →+* N) = B} =
      Nat.card T * Module.finrank κ N := by
    rw [← KFA2a.card_stabilizer_algHom K act hact,
      ← KFA2a.card_smul_mem (IsScalarTower.toAlgHom K κ N) T (fun τ _ => horbit τ) (Set.toFinite T)]
    rfl
  have h2 : Nat.card T = Nat.card {σ : κ →ₐ[K] L // A.comap (σ : κ →+* L) = B} := by
    refine Nat.card_congr ((normalClosure.algHomEquiv K κ L).subtypeEquiv fun τ => ?_)
    change (A.comap (ι : N →+* L)).comap (τ : κ →+* N) = B ↔
      A.comap ((normalClosure.algHomEquiv K κ L τ : κ →ₐ[K] L) : κ →+* L) = B
    have : (A.comap (ι : N →+* L)).comap (τ : κ →+* N) =
        A.comap ((normalClosure.algHomEquiv K κ L τ : κ →ₐ[K] L) : κ →+* L) := by
      ext x; simp only [ValuationSubring.mem_comap, RingHom.coe_coe]; rfl
    rw [this]
  have hpos : 0 < Module.finrank κ N := by
    have : Module.Finite κ N := Module.Finite.of_restrictScalars_finite K κ N
    exact Module.finrank_pos
  have h3 : Nat.card T = KFA2a.ef B hCB := by
    have := h1.symm.trans hcount
    rw [mul_comm] at this
    exact Nat.eq_of_mul_eq_mul_left hpos this
  rw [← h2, h3]
  rfl

Module documentation

Valuation Subring nat Card alg Hom comap eq ramification Idx mul inertia Deg

Declarations