Module

IntegralClosure.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.IntegralClosure

9 declarations indexed from sourceView source ↗

Module documentation

Extending finiteness to an integral-closure model

A valuation ring is integrally closed in its fraction field. Consequently, if a prime divisor is finite on a model A, it is finite on the integral closure of A in the ambient field. This is the bridge from an affine coordinate model to the Dedekind normalization used in the prime counts of Fried--Jarden, Lemma 6.2.2.

Imports3

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Valuation.LocalSubring

Imported by3

def

integralClosureModel

L36 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.integralClosureModel

Documentation

The integral closure in F of a K-subalgebra A, regarded again as a K-subalgebra of F.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

def integralClosureModel (A : Subalgebra K F) : Subalgebra K F

theorem

integralClosureModel_coe

L40 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.integralClosureModel_coe

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem integralClosureModel_coe
    (A : Subalgebra K F) (x : integralClosureModel A) :
    ((x : integralClosureModel A) : F) = x

theorem

finiteOn_integralClosureModel

L51 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOn_integralClosureModel

Documentation

Finiteness on a model extends to its integral closure in the ambient field.

No finiteness assumption on the normalization is needed: every element is integral over A, and the valuation ring is integrally closed.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finiteOn_integralClosureModel
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (hfinite : v.FiniteOn A) :
    v.FiniteOn (integralClosureModel A)

theorem

finiteAlong_integralClosure

L79 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteAlong_integralClosure

Documentation

Finiteness along an algebra model extends to any realization of its integral closure in the ambient field.

The algebra structures on the source and the integral-closure model are explicit inputs. Only the valuation-subring algebra needed by the integrality argument is installed locally, so downstream proofs do not have to reconstruct that instance tower.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finiteAlong_integralClosure
    {A B : Type*} [CommRing A] [CommRing B]
    [Algebra K A] [Algebra K B] [Algebra A B]
    [Algebra A F] [Algebra B F]
    [IsScalarTower K A F] [IsScalarTower K B F]
    [IsScalarTower A B F] [IsIntegralClosure B A F]
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong (IsScalarTower.toAlgHom K A F)) :
    v.FiniteAlong (IsScalarTower.toAlgHom K B F)

theorem

integralClosure_isTorsionFree_of_algebraMap_injective

L110 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.integralClosure_isTorsionFree_of_algebraMap_injective

Documentation

An integral-closure model is torsion-free over the base as soon as the base embeds in the ambient field. Supplying the injectivity proof explicitly avoids asking typeclass synthesis to rediscover a FaithfulSMul path through the surrounding algebra tower.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem integralClosure_isTorsionFree_of_algebraMap_injective
    {A B : Type*} [CommRing A] [IsDomain A] [CommRing B]
    [Algebra A B] [Algebra A F] [Algebra B F]
    [IsScalarTower A B F] [IsIntegralClosure B A F]
    (hF : Function.Injective (algebraMap A F)) :
    Module.IsTorsionFree A B

theorem

finiteOn_of_le

L121 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteOn_of_le

Documentation

Finiteness descends along an inclusion of models.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finiteOn_of_le
    (v : FunctionFieldPrimeDivisor K F)
    {A B : Subalgebra K F} (hAB : A ≤ B)
    (hfinite : v.FiniteOn B) :
    v.FiniteOn A

theorem

center_comap_of_le

L131 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.center_comap_of_le

Documentation

Centers are compatible with contraction along an inclusion of models.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem center_comap_of_le
    (v : FunctionFieldPrimeDivisor K F)
    {A B : Subalgebra K F} (hAB : A ≤ B)
    (hfinite : v.FiniteOn B) :
    (v.center B hfinite).comap
        (Subalgebra.inclusion hAB).toRingHom =
      v.center A (v.finiteOn_of_le hAB hfinite)

theorem

le_integralClosureModel

L144 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.le_integralClosureModel

Documentation

The original model is contained in its integral closure model.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem le_integralClosureModel (A : Subalgebra K F) :
    A ≤ integralClosureModel A

theorem

center_integralClosureModel_comap

L156 ↗

FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.center_integralClosureModel_comap

Documentation

The center on the integral closure contracts to the original center.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem center_integralClosureModel_comap
    (v : FunctionFieldPrimeDivisor K F) (A : Subalgebra K F)
    (hfinite : v.FiniteOn A) :
    (v.center (integralClosureModel A)
        (v.finiteOn_integralClosureModel A hfinite)).comap
        (Subalgebra.inclusion (le_integralClosureModel A)).toRingHom =
      v.center A hfinite

Module documentation

Extending finiteness to an integral-closure model

Declarations