Module

StrictHenselianFiniteDomainPointLift.lean

Nyll.SchemeTheory.RingTheory.StrictHenselianFiniteDomainPointLift

1 declaration indexed from sourceView source ↗

Module documentation

Lifting a specified geometric closed point to a finite domain

The prescribed local map to an algebraically closed field induces the scalar map on the base residue field. The finite residue extension embeds over that scalar map into the same field. Composing with the residue map constructs a local point over the prescribed one. Strict Henselianity then makes every automorphism of the finite algebra fix this constructed point.

Imports3

Nyll.SchemeTheory.RingTheory.StrictHenselianFiniteDomainPoint
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by2

theorem

exists_local_hom_finiteDomain_fixed_of_strictHenselian

L30 ↗

SchemeTheory.exists_local_hom_finiteDomain_fixed_of_strictHenselian

Documentation

A specified geometric closed point of a strictly Henselian local ring lifts to a finite domain algebra over the same algebraically closed field, and every algebra automorphism fixes the resulting 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 exists_local_hom_finiteDomain_fixed_of_strictHenselian
    (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 Ω] [IsAlgClosed Ω] (ψ : R →+* Ω) [IsLocalHom ψ] :
    ∃ φ : B →+* Ω, IsLocalHom φ ∧ φ.comp (algebraMap R B) = ψ ∧
      ∀ σ : B ≃ₐ[R] B, φ.comp σ.toRingEquiv.toRingHom = φ

Module documentation

Lifting a specified geometric closed point to a finite domain

Declarations

exists_local_hom_finiteDomain_fixed_of_strictHenselian