Module

HenselianIntegralClosureUnits.lean

Nyll.SchemeTheory.RingTheory.HenselianIntegralClosureUnits

5 declarations indexed from sourceView source ↗

Module documentation

Units of integral elements over a Henselian base

The integral closure of a Henselian local ring in a field is local. Inside a normal local ring with that fraction field, the integral closure embeds by the native integral-element constructor. Its map is local because its maximal-ideal contraction lies over the maximal ideal of the base. Consequently a base-linear field automorphism preserves whether an integral element is a unit in the specified normal local ring.

Imports5

Nyll.SchemeTheory.RingTheory.HenselianIntegralDomainLocal
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by2

def

integralClosureToNormalRing

L37 ↗

SchemeTheory.integralClosureToNormalRing

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Lift
variable (R : Type u) (T : Type v) (L : Type w)
  [CommRing R] [CommRing T] [IsIntegrallyClosed T]
  [Field L] [Algebra R T] [Algebra T L] [IsFractionRing T L]
  [Algebra R L] [IsScalarTower R T L]

Lean source · full declaration

def integralClosureToNormalRing : integralClosure R L →+* T where
  toFun c := IsIntegralClosure.mk' T (c : L) (c.property.tower_top (A := T))
  map_one' := IsIntegralClosure.mk'_one (R := T) T
  map_zero' := IsIntegralClosure.mk'_zero (R := T) T
  map_add' c d := IsIntegralClosure.mk'_add T (c : L) (d : L)
    (c.property.tower_top (A := T)) (d.property.tower_top (A := T))
  map_mul' c d := IsIntegralClosure.mk'_mul T (c : L) (d : L)
    (c.property.tower_top (A := T)) (d.property.tower_top (A := T))

theorem

integralClosureToNormalRing_evaluation

L46 ↗

SchemeTheory.integralClosureToNormalRing_evaluation

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Lift
variable (R : Type u) (T : Type v) (L : Type w)
  [CommRing R] [CommRing T] [IsIntegrallyClosed T]
  [Field L] [Algebra R T] [Algebra T L] [IsFractionRing T L]
  [Algebra R L] [IsScalarTower R T L]

Lean source · statement

theorem integralClosureToNormalRing_evaluation (c : integralClosure R L) :
    algebraMap T L (integralClosureToNormalRing R T L c) = (c : L)

theorem

integralClosureToNormalRing_comp

L50 ↗

SchemeTheory.integralClosureToNormalRing_comp

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Lift
variable (R : Type u) (T : Type v) (L : Type w)
  [CommRing R] [CommRing T] [IsIntegrallyClosed T]
  [Field L] [Algebra R T] [Algebra T L] [IsFractionRing T L]
  [Algebra R L] [IsScalarTower R T L]

Lean source · statement

theorem integralClosureToNormalRing_comp :
    (integralClosureToNormalRing R T L).comp (algebraMap R (integralClosure R L)) =
      algebraMap R T

theorem

integralClosureToNormalRing_isLocalHom

L70 ↗

SchemeTheory.integralClosureToNormalRing_isLocalHom

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Local
variable (R : Type u) (T : Type v) (L : Type w)
  [CommRing R] [HenselianLocalRing R]
  [CommRing T] [IsIntegrallyClosed T] [IsLocalRing T]
  [Field L] [Algebra R T] [Algebra T L] [IsFractionRing T L]
  [Algebra R L] [IsScalarTower R T L] [IsLocalHom (algebraMap R T)]

Lean source · statement

theorem integralClosureToNormalRing_isLocalHom :
    IsLocalHom (integralClosureToNormalRing R T L)

theorem

isUnit_iff_of_henselian_integral_conjugate

L94 ↗

SchemeTheory.isUnit_iff_of_henselian_integral_conjugate

Documentation

A base-linear automorphism of the fraction field preserves unit status for elements integral over the Henselian local base, in the given normal local overring. Both elements and their equality in the field are actual input elements; no extension of the automorphism to the overring is assumed.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Local
variable (R : Type u) (T : Type v) (L : Type w)
  [CommRing R] [HenselianLocalRing R]
  [CommRing T] [IsIntegrallyClosed T] [IsLocalRing T]
  [Field L] [Algebra R T] [Algebra T L] [IsFractionRing T L]
  [Algebra R L] [IsScalarTower R T L] [IsLocalHom (algebraMap R T)]

Lean source · statement

theorem isUnit_iff_of_henselian_integral_conjugate
    (e : L ≃ₐ[R] L) (t t' : T)
    (ht : IsIntegral R (algebraMap T L t))
    (he : algebraMap T L t' = e (algebraMap T L t)) :
    IsUnit t' ↔ IsUnit t

Module documentation

Units of integral elements over a Henselian base

Declarations

integralClosureToNormalRing

integralClosureToNormalRing_evaluation

integralClosureToNormalRing_comp

integralClosureToNormalRing_isLocalHom

isUnit_iff_of_henselian_integral_conjugate