Module

PointSpecialization.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.PointSpecialization

12 declarations indexed from sourceView source ↗

Module documentation

Specializing finite étale points through a normal Henselian local ring

For an integral algebra over the base, every point in a normal local ring's fraction field has a unique factorization through that ring. This uses its normal self-integral-closure structure, not integrality of the local ring over the base. For an étale algebra, the existing Henselian section theorem identifies local-ring points with residue-field points through its actual target-lifting bijection. Their composite is the actual specialization equivalence, natural in the finite étale algebra and equivariant for compatible actual actions.

Imports7

Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianEtaleMapLift
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.Etale.Basic

Imported by3

def

integralPointLift

L43 ↗

SchemeTheory.integralPointLift

Documentation

An integral algebra's fraction-field point factors through the actual normal ring, by its native self-integral-closure constructor.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section IntegralPoints
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Algebra.IsIntegral H T]

Lean source · full declaration

def integralPointLift (f : T →ₐ[H] L) : T →ₐ[H] R where
  toFun a := IsIntegralClosure.mk' R (f a)
    (((Algebra.IsIntegral.isIntegral (R := H) a).map f).tower_top (A := R))
  map_one' := by
    apply IsFractionRing.injective R L
    simp only [IsIntegralClosure.algebraMap_mk', map_one]
  map_zero' := by
    apply IsFractionRing.injective R L
    simp only [IsIntegralClosure.algebraMap_mk', map_zero]
  map_add' a b := by
    apply IsFractionRing.injective R L
    simp only [IsIntegralClosure.algebraMap_mk', map_add]
  map_mul' a b := by
    apply IsFractionRing.injective R L
    simp only [IsIntegralClosure.algebraMap_mk', map_mul]
  commutes' h := by
    apply IsFractionRing.injective R L
    exact (IsIntegralClosure.algebraMap_mk' R (f (algebraMap H T h))
      (((Algebra.IsIntegral.isIntegral (R := H)
        (algebraMap H T h)).map f).tower_top (A := R))).trans
        ((f.commutes h).trans (IsScalarTower.algebraMap_apply H R L h))

theorem

integralPointLift_evaluation

L65 ↗

SchemeTheory.integralPointLift_evaluation

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section IntegralPoints
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Algebra.IsIntegral H T]

Lean source · statement

theorem integralPointLift_evaluation (f : T →ₐ[H] L) (a : T) :
    algebraMap R L (integralPointLift H R L T f a) = f a

def

integralPointEquiv

L72 ↗

SchemeTheory.integralPointEquiv

Documentation

Composition with the actual fraction-field inclusion gives a bijection on points of every integral algebra over the base.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section IntegralPoints
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Algebra.IsIntegral H T]

Lean source · full declaration

def integralPointEquiv : (T →ₐ[H] R) ≃ (T →ₐ[H] L) where
  toFun f := (IsScalarTower.toAlgHom H R L).comp f
  invFun := integralPointLift H R L T
  left_inv f := by
    apply AlgHom.ext
    intro a
    apply IsFractionRing.injective R L
    exact integralPointLift_evaluation H R L T _ a
  right_inv f := by
    apply AlgHom.ext
    intro a
    exact integralPointLift_evaluation H R L T f a

theorem

integralPointLift_naturality

L85 ↗

SchemeTheory.integralPointLift_naturality

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section IntegralPoints
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Algebra.IsIntegral H T]

Lean source · statement

theorem integralPointLift_naturality
    {U : Type u} [CommRing U] [Algebra H U] [Algebra.IsIntegral H U]
    (g : U →ₐ[H] T) (f : T →ₐ[H] L) :
    integralPointLift H R L U (f.comp g) = (integralPointLift H R L T f).comp g

def

henselianPointReductionEquiv

L104 ↗

SchemeTheory.henselianPointReductionEquiv

Documentation

The existing Henselian target-lifting bijection, expressed using the native residue-field algebra and the original base algebra.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section HenselianReduction
variable (H R T : Type u) [CommRing H] [CommRing R] [HenselianLocalRing R]
  [Algebra H R] [CommRing T] [Algebra H T] [Algebra.Etale H T]

Lean source · statement

def henselianPointReductionEquiv :
    (T →ₐ[H] R) ≃ (T →ₐ[H] IsLocalRing.ResidueField R)

theorem

henselianPointReductionEquiv_apply

L114 ↗

SchemeTheory.henselianPointReductionEquiv_apply

Documentation

This equivalence is actual reduction, evaluated on every algebra element.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section HenselianReduction
variable (H R T : Type u) [CommRing H] [CommRing R] [HenselianLocalRing R]
  [Algebra H R] [CommRing T] [Algebra H T] [Algebra.Etale H T]

Lean source · statement

theorem henselianPointReductionEquiv_apply (f : T →ₐ[H] R) (a : T) :
    henselianPointReductionEquiv H R T f a = IsLocalRing.residue R (f a)

def

residueAlgEquiv

L126 ↗

SchemeTheory.residueAlgEquiv

Documentation

The native residue-field equivalence of an actual base-linear local-ring automorphism, with its inherited original base-algebra structure.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section ResidueAction
variable (H R : Type u) [CommRing H] [CommRing R] [IsLocalRing R] [Algebra H R]

Lean source · statement

def residueAlgEquiv (τ : R ≃ₐ[H] R) :
    IsLocalRing.ResidueField R ≃ₐ[H] IsLocalRing.ResidueField R

theorem

residueAlgEquiv_residue

L138 ↗

SchemeTheory.residueAlgEquiv_residue

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section ResidueAction
variable (H R : Type u) [CommRing H] [CommRing R] [IsLocalRing R] [Algebra H R]

Lean source · statement

theorem residueAlgEquiv_residue (τ : R ≃ₐ[H] R) (r : R) :
    residueAlgEquiv H R τ (IsLocalRing.residue R r) = IsLocalRing.residue R (τ r)

def

finiteEtalePointSpecialization

L156 ↗

SchemeTheory.finiteEtalePointSpecialization

Documentation

The actual specialization equivalence from generic points to residue points of a finite étale algebra, through the given normal Henselian ring.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section Specialization
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Module.Finite H T] [Algebra.Etale H T]

Lean source · statement

def finiteEtalePointSpecialization :
    (T →ₐ[H] L) ≃ (T →ₐ[H] IsLocalRing.ResidueField R)

theorem

finiteEtalePointSpecialization_apply

L160 ↗

SchemeTheory.finiteEtalePointSpecialization_apply

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section Specialization
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Module.Finite H T] [Algebra.Etale H T]

Lean source · statement

theorem finiteEtalePointSpecialization_apply (f : T →ₐ[H] L) (a : T) :
    finiteEtalePointSpecialization H R L T f a =
      IsLocalRing.residue R (integralPointLift H R L T f a)

theorem

finiteEtalePointSpecialization_naturality

L166 ↗

SchemeTheory.finiteEtalePointSpecialization_naturality

Documentation

Specialization commutes with the actual morphisms of finite étale algebras.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section Specialization
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Module.Finite H T] [Algebra.Etale H T]

Lean source · statement

theorem finiteEtalePointSpecialization_naturality
    {U : Type u} [CommRing U] [Algebra H U] [Module.Finite H U] [Algebra.Etale H U]
    (g : U →ₐ[H] T) (f : T →ₐ[H] L) :
    finiteEtalePointSpecialization H R L U (f.comp g) =
      (finiteEtalePointSpecialization H R L T f).comp g

theorem

finiteEtalePointSpecialization_equivariant

L181 ↗

SchemeTheory.finiteEtalePointSpecialization_equivariant

Documentation

The same specialization is equivariant for compatible actual automorphisms of the normal local ring and its fraction field. The residue action is the native map of residue fields, with no action assumed on the point set.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v
section Specialization
variable (H R : Type u) (L : Type v) (T : Type u)
  [CommRing H] [CommRing R] [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [CommRing T] [Algebra H T] [Module.Finite H T] [Algebra.Etale H T]

Lean source · statement

theorem finiteEtalePointSpecialization_equivariant
    (τ : R ≃ₐ[H] R) (σ : L ≃ₐ[H] L)
    (hσ : ∀ r : R, σ (algebraMap R L r) = algebraMap R L (τ r))
    (f : T →ₐ[H] L) :
    finiteEtalePointSpecialization H R L T (σ.toAlgHom.comp f) =
      (residueAlgEquiv H R τ).toAlgHom.comp (finiteEtalePointSpecialization H R L T f)

Module documentation

Specializing finite étale points through a normal Henselian local ring

Declarations