NYLL
Module

IntegrallyClosed.lean

Nyll.EtaleFundamentalGroups.Kummer.IteratedRadical.IntegrallyClosed
2 declarations indexed from sourceView source ↗

Module documentation

Normality of two-dimensional iterated radical covers

A positive iterated radical cover of a two-dimensional regular parameter pair again has an explicit regular parameter pair generating its maximal ideal. The dimension-two conductor criterion therefore shows directly that the cover is integrally closed.

Imports2
Imported by1

Declarations

theorem

exists_pair_of_length_eq_two

L28 ↗
EtaleFundamentalGroups.Kummer.exists_pair_of_length_eq_two
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem exists_pair_of_length_eq_two {R : Type u} (xs : List R)
    (hxs : xs.length = 2) :
    ∃ x y : R, xs = [x, y]
theorem

isIntegrallyClosed_iteratedRadical_of_regular_pair

L43 ↗
EtaleFundamentalGroups.Kummer.isIntegrallyClosed_iteratedRadical_of_regular_pair
Documentation

The full positive iterated radical cover of a two-dimensional regular parameter pair is integrally closed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
open RingTheory.Sequence
universe u
Lean source · statement
theorem isIntegrallyClosed_iteratedRadical_of_regular_pair
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (n : Fin 2 → ℕ) (a : Fin 2 → A)
    (hn : ∀ i, 0 < n i)
    (hreg : IsRegular A (List.ofFn a))
    (hgen : Ideal.ofList (List.ofFn a) = maximalIdeal A) :
    IsIntegrallyClosed (iteratedRadical A 2 n a)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.