NYLL
Module

ChosenResidueExtension.lean

Nyll.SchemeTheory.Etale.ChosenResidueExtension
2 declarations indexed from sourceView source ↗

Module documentation

An étale base extension adapted to one quasi-finite point

Realize the separable closure of the base residue field inside the selected residue field in an étale neighborhood. Evaluation into the selected residue field defines a prime of the tensor product. The induced residue map is an isomorphism, while the extension from the new base residue field is purely inseparable.

Imports9
  • Nyll.SchemeTheory.Etale.ResidueFieldExtension
  • Mathlib.FieldTheory.IntermediateField.Algebraic
  • Mathlib.FieldTheory.PurelyInseparable.Basic
  • Mathlib.FieldTheory.SeparableClosure
  • Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.QuasiFinite.Basic
  • Mathlib.RingTheory.RingHom.PurelyInseparable
  • Mathlib.RingTheory.TensorProduct.Maps
Imported by2

Declarations

theorem

ringEquiv_isPurelyInseparable

L38 ↗
Algebra.Etale.ringEquiv_isPurelyInseparable
Source context 4 commands

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

@[expose] public section
open scoped TensorProduct
universe u v
namespace Algebra.Etale
Lean source · statement
theorem ringEquiv_isPurelyInseparable
    {K L : Type*} [Field K] [Field L] (e : K ≃+* L) :
    e.toRingHom.IsPurelyInseparable
theorem

exists_chosen_residue_extension

L49 ↗
Algebra.Etale.exists_chosen_residue_extension
Documentation

After an actual étale base extension, a chosen point of a quasi-finite algebra has the same residue field as before and is purely inseparable over the new base residue field. The tensor-product prime is constructed as an evaluation kernel, and the residue-field isomorphism is compatible with the old point.

Source context 4 commands

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

@[expose] public section
open scoped TensorProduct
universe u v
namespace Algebra.Etale
Lean source · statement
theorem exists_chosen_residue_extension
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.QuasiFinite R S] (p : Ideal R) [p.IsPrime]
    (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    ∃ (R' : Type u) (_ : CommRing R') (_ : Algebra R R') (_ : Algebra.Etale R R')
      (P : Ideal R') (_ : P.IsPrime) (_ : P.LiesOver p)
      (Q : Ideal (R' ⊗[R] S)) (_ : Q.IsPrime) (_ : Q.LiesOver P)
      (hq : q = Q.comap
        (Algebra.TensorProduct.includeRight : S →ₐ[R] R' ⊗[R] S).toRingHom)
      (e : Q.ResidueField ≃+* q.ResidueField),
      e.toRingHom.comp (Ideal.ResidueField.map q Q
        (Algebra.TensorProduct.includeRight : S →ₐ[R] R' ⊗[R] S).toRingHom hq) =
          RingHom.id q.ResidueField ∧
      (Ideal.ResidueField.map P Q (algebraMap R' (R' ⊗[R] S))
        (Q.over_def P)).IsPurelyInseparable

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