Module

StrictHenselianFiniteDomainPoint.lean

Nyll.SchemeTheory.RingTheory.StrictHenselianFiniteDomainPoint

1 declaration indexed from sourceView source ↗

Module documentation

Closed geometric points of finite domains over strictly Henselian rings

A finite domain over a Henselian local ring is local. When the base residue field is separably closed, its finite residue extension is purely inseparable. Thus every automorphism of the finite algebra fixes every closed geometric point. The locality and the residue action are both proved here.

Imports3

Nyll.SchemeTheory.RingTheory.HenselianFiniteDomainLocal
Mathlib.FieldTheory.PurelyInseparable.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by2

theorem

strictHenselian_finiteDomain_aut_fixes_closedPoint

L28 ↗

SchemeTheory.strictHenselian_finiteDomain_aut_fixes_closedPoint

Documentation

Every algebra automorphism of a finite domain over a strictly Henselian local ring fixes a specified closed geometric point.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w

Lean source · statement

theorem strictHenselian_finiteDomain_aut_fixes_closedPoint
    (R : Type u) (B : Type v) [CommRing R] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    [CommRing B] [IsDomain B] [Algebra R B] [Module.Finite R B]
    {Ω : Type w} [Field Ω] (φ : B →+* Ω) [IsLocalHom φ]
    (σ : B ≃ₐ[R] B) : φ.comp σ.toRingEquiv.toRingHom = φ

Module documentation

Closed geometric points of finite domains over strictly Henselian rings

Declarations

strictHenselian_finiteDomain_aut_fixes_closedPoint