Module

IntegrallyClosed.lean

Nyll.EtaleFundamentalGroups.Kummer.Laurent.IntegrallyClosed

4 declarations indexed from sourceView source ↗

Module documentation

Integral closedness of finite lattice Laurent algebras

A one-variable Laurent algebra is the localization of a polynomial ring away from X. Polynomial rings over integrally closed domains are integrally closed, and integral closedness survives this localization. Iterating this construction and transporting along the explicit finite-coordinate Laurent equivalence gives the result for the lattice target in the Smith presentation.

Imports4

Mathlib.Algebra.Polynomial.Laurent
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.Polynomial.IsIntegral

Imported by2

theorem

isIntegrallyClosed_addMonoidAlgebra_int

L30 ↗

EtaleFundamentalGroups.Kummer.isIntegrallyClosed_addMonoidAlgebra_int

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u
open Polynomial

Lean source · statement

theorem isIntegrallyClosed_addMonoidAlgebra_int
    {A : Type u} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] :
    IsIntegrallyClosed (AddMonoidAlgebra A ℤ)

def

finLastInitAddEquiv

L40 ↗

EtaleFundamentalGroups.Kummer.finLastInitAddEquiv

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u
open Polynomial

Lean source · statement

def finLastInitAddEquiv (r : ℕ) :
    (Fin (r + 1) → ℤ) ≃+ (ℤ × (Fin r → ℤ))

theorem

isIntegrallyClosed_finLaurent

L48 ↗

EtaleFundamentalGroups.Kummer.isIntegrallyClosed_finLaurent

Documentation

A Laurent algebra on finitely many independent integer coordinates is integrally closed.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u
open Polynomial

Lean source · statement

theorem isIntegrallyClosed_finLaurent
    {R : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    (r : ℕ) : IsIntegrallyClosed (AddMonoidAlgebra R (Fin r → ℤ))

theorem

latticeMonoidAlgebra_isIntegrallyClosed

L66 ↗

EtaleFundamentalGroups.Kummer.latticeMonoidAlgebra_isIntegrallyClosed

Documentation

The Laurent algebra of a finite free integer lattice is integrally closed.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u
open Polynomial

Lean source · statement

theorem latticeMonoidAlgebra_isIntegrallyClosed
    {R L : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L] :
    IsIntegrallyClosed (AddMonoidAlgebra R L)

Module documentation

Integral closedness of finite lattice Laurent algebras

Declarations

isIntegrallyClosed_addMonoidAlgebra_int

finLastInitAddEquiv

isIntegrallyClosed_finLaurent

latticeMonoidAlgebra_isIntegrallyClosed