NYLL
Module

NormalizationAbsoluteResidueClosure.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationAbsoluteResidueClosure
3 declarations indexed from sourceView source ↗

Module documentation

Algebraic closedness of absolute normalization residues

Proves that the maximal quotient of the normalization of a DVR in a separable closure of its fraction field is algebraically closed.

Imports5
Imported by3

Declarations

theorem

normalizationMaximalPrime_ne_bot

L30 ↗
EtaleFundamentalGroups.Inertia.normalizationMaximalPrime_ne_bot
Documentation

A maximal prime of the actual normalization is nonzero because its contraction is the nonzero maximal ideal of the original DVR.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem normalizationMaximalPrime_ne_bot
    (A : Type u) (Ω : Type w) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field Ω] [Algebra A Ω] [FaithfulSMul A Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] : Q ≠ ⊥
theorem

normalizationMaximalQuotient_isAlgClosed_of_algebraic

L47 ↗
EtaleFundamentalGroups.Inertia.normalizationMaximalQuotient_isAlgClosed_of_algebraic
Documentation

Algebraicity and the actual faithful coefficient map supply the fraction field of the normalization before the residue theorem is applied.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem normalizationMaximalQuotient_isAlgClosed_of_algebraic
    (A : Type u) (Ω : Type w) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field Ω] [Algebra A Ω] [FaithfulSMul A Ω]
    [Algebra.IsAlgebraic A Ω] [IsSepClosed Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    IsAlgClosed ((normalizationCommAlgCat A Ω) ⧸ Q)
theorem

normalizationAbsoluteResidue_isAlgClosed

L66 ↗
EtaleFundamentalGroups.Inertia.normalizationAbsoluteResidue_isAlgClosed
Documentation

The literal residue quotient at the chosen original absolute normalization prime is algebraically closed in every characteristic.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem normalizationAbsoluteResidue_isAlgClosed
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
    (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal] :
    IsAlgClosed ((normalizationCommAlgCat A Ω) ⧸ Q)

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