NYLL
Module

FiniteResidueGeometricPoint.lean

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

Module documentation

Geometric points of finite algebras over a local ring

Every maximal ideal of a finite algebra above the closed point can be represented over the same chosen algebraic closure of the base residue field. The resulting ring map has the given kernel and the canonical base map.

Imports4
  • Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
  • Mathlib.RingTheory.Ideal.Over
  • Mathlib.RingTheory.Finiteness.Quotient
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
Imported by2

Declarations

theorem

exists_finite_residue_geometricPoint

L28 ↗
SchemeTheory.exists_finite_residue_geometricPoint
Documentation

A closed point of a finite algebra lifts to the fixed algebraic closure of the local base's residue field, preserving the actual base map.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
theorem exists_finite_residue_geometricPoint
    (R : Type u) [CommRing R] [IsLocalRing R]
    (B : Type v) [CommRing B] [Algebra R B] [Module.Finite R B]
    (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal R)] :
    ∃ φ : B →+* AlgebraicClosure (IsLocalRing.ResidueField R),
      RingHom.ker φ = Q ∧
      φ.comp (algebraMap R B) =
        (algebraMap (IsLocalRing.ResidueField R)
          (AlgebraicClosure (IsLocalRing.ResidueField R))).comp (IsLocalRing.residue R)

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