Module

NativeNormalizationRadical.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeNormalizationRadical

2 declarations indexed from sourceView source ↗

Module documentation

Ambient integral radicals in the actual native subalgebra normalization

Literal membership in the subalgebra and the already proved ambient integrality construct the actual normalization element. Its power equation is inherited through the two subtype inclusions. No fraction-field tower or chosen absolute prime is opened in this owner.

Imports3

Nyll.SchemeTheory.Normalization.SubalgebraPreimage
Nyll.SchemeTheory.CategoryTheory.CommAlgRingMap
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by2

def

nativeNormalizationElement

L32 ↗

EtaleFundamentalGroups.Inertia.nativeNormalizationElement

Documentation

An actual integral ambient element in the selected subalgebra gives an element of its literal native normalization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable {A : Type u} {Ω : Type v} [CommRing A] [CommRing Ω] [Algebra A Ω]

Lean source · statement

def nativeNormalizationElement
    (S : Subalgebra A Ω) (α : Ω) (hmem : α ∈ S) (hint : IsIntegral A α) :
    subalgebraNormalizationCommAlgCat S

theorem

nativeNormalizationElement_pow

L39 ↗

EtaleFundamentalGroups.Inertia.nativeNormalizationElement_pow