Module

AbsoluteResidueClosure.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteResidueClosure

3 declarations indexed from sourceView source ↗

Module documentation

The literal maximal quotient in the absolute residue-closure argument

The established separably closed fraction-field theorem applies to the prime residue field. At a maximal ideal its canonical quotient map is bijective, so algebraic closedness transfers to the actual quotient. A separate integral-ring owner proves algebraicity over the contracted quotient, without carrying the fraction field or its scalar structures.

Reference: Stacks Project, Tag 0BUB. https://stacks.math.columbia.edu/tag/0BUB

Imports3

Nyll.EtaleFundamentalGroups.StrictHenselian.SeparablyClosedFractionResidue
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Imported by2

theorem

maximalQuotient_isAlgClosed_of_primeResidueField

L32 ↗

EtaleFundamentalGroups.Inertia.maximalQuotient_isAlgClosed_of_primeResidueField

Documentation

The canonical map identifies a maximal quotient with the prime residue field, so splitting transfers to the literal quotient.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem maximalQuotient_isAlgClosed_of_primeResidueField
    (B : Type u) [CommRing B] (Q : Ideal B) [Q.IsMaximal]
    [IsAlgClosed Q.ResidueField] : IsAlgClosed (B ⧸ Q)

theorem

maximalQuotient_isAlgClosed_of_isSepClosed_fractionRing

L45 ↗

EtaleFundamentalGroups.Inertia.maximalQuotient_isAlgClosed_of_isSepClosed_fractionRing

Documentation

The literal maximal quotient of a normal domain with separably closed fraction field is algebraically closed whenever the maximal ideal is nonzero. No perfectness or residue characteristic assumption is made.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem maximalQuotient_isAlgClosed_of_isSepClosed_fractionRing
    (B : Type u) (Ω : Type v) [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Field Ω] [Algebra B Ω] [IsFractionRing B Ω] [IsSepClosed Ω]
    (Q : Ideal B) [Q.IsMaximal] (hQ : Q ≠ ⊥) : IsAlgClosed (B ⧸ Q)

theorem

maximalQuotient_isAlgClosure_of_isIntegral

L56 ↗

EtaleFundamentalGroups.Inertia.maximalQuotient_isAlgClosure_of_isIntegral

Documentation

Integrality descends to the actual quotient by a maximal ideal and its contraction. Thus an algebraically closed upper quotient is an algebraic closure of the lower quotient.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem maximalQuotient_isAlgClosure_of_isIntegral
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Algebra.IsIntegral A B] (Q : Ideal B) [Q.IsMaximal]
    [IsAlgClosed (B ⧸ Q)] : IsAlgClosure (A ⧸ Q.under A) (B ⧸ Q)

Module documentation

The literal maximal quotient in the absolute residue-closure argument

Declarations

maximalQuotient_isAlgClosed_of_primeResidueField

maximalQuotient_isAlgClosed_of_isSepClosed_fractionRing

maximalQuotient_isAlgClosure_of_isIntegral