NYLL
Module

HenselianFiniteDomainLocal.lean

Nyll.SchemeTheory.RingTheory.HenselianFiniteDomainLocal
1 declaration indexed from sourceView source ↗

Module documentation

Finite domains over Henselian local rings are local

The special fiber is an Artinian algebra. Two distinct maximal ideals would be separated by an idempotent in that fiber. Henselian lifting produces an idempotent in the domain, which must be zero or one, a contradiction.

Imports3
Imported by3

Declarations

theorem

isLocalRing_of_finite_domain_henselian

L25 ↗
SchemeTheory.isLocalRing_of_finite_domain_henselian
Documentation

A finite algebra which is a domain over a Henselian local ring has a unique maximal ideal. No locality assumption on the finite algebra is used.

Source context 2 commands

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

namespace SchemeTheory
universe u v
Lean source · statement
theorem isLocalRing_of_finite_domain_henselian
    (R : Type u) (B : Type v) [CommRing R] [HenselianLocalRing R]
    [CommRing B] [IsDomain B] [Algebra R B] [Module.Finite R B] :
    IsLocalRing B

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