Module

IntegralClosureTorsion.lean

Nyll.GaloisCohomology.FieldTheory.IntegralClosureTorsion

2 declarations indexed from sourceView source ↗

Module documentation

Imports2

Imported by3

theorem

FieldTheory.isIntegral_torsionUnit

Documentation

Roots of unity are integral over any coefficient ring.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K]

Lean source · statement

theorem isIntegral_torsionUnit (z : Kˣ) (hz : IsOfFinOrder z) :
    IsIntegral R (z : K)

def

FieldTheory.torsionUnitsIntegralClosureEquiv

Documentation

Every torsion unit has a unique lift to a torsion unit in the integral closure.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K]

Lean source · statement

def torsionUnitsIntegralClosureEquiv :
    CommGroup.torsion Kˣ ≃* CommGroup.torsion (integralClosure R K)ˣ