NYLL
Module

SubalgebraResidueFieldColimit.lean

Nyll.SchemeTheory.RingTheory.SubalgebraResidueFieldColimit
13 declarations indexed from sourceView source ↗

Module documentation

Residue fields of exhaustive subalgebra stages

For an exhaustive directed family of subalgebras, contraction of one prime of the ambient ring gives a diagram of actual residue fields. Its canonical cocone has the ambient residue field as its colimit: every fraction has numerator and denominator in a common stage, and every cocone leg is injective.

Imports5
  • Mathlib.Algebra.Category.Ring.FilteredColimits
  • Mathlib.Algebra.Category.Ring.Colimits
  • Mathlib.CategoryTheory.Limits.Types.Filtered
  • Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
Imported by2

Declarations

abbrev

residuePrime

L36 ↗
AlgebraicGeometry.SubalgebraStages.residuePrime
Documentation

The prime at a stage obtained by contracting the original ambient prime.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
abbrev residuePrime (i : ι) : Ideal (S i)
def

residueTrans

L40 ↗
AlgebraicGeometry.SubalgebraStages.residueTrans
Documentation

The map on actual residue fields induced by a stage inclusion.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
def residueTrans {i j : ι} (h : i ≤ j) :
    (residuePrime S p i).ResidueField →+* (residuePrime S p j).ResidueField
def

residueLeg

L46 ↗
AlgebraicGeometry.SubalgebraStages.residueLeg
Documentation

The actual residue-field embedding induced by inclusion in the ambient ring.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
def residueLeg (i : ι) : (residuePrime S p i).ResidueField →+* p.ResidueField
lemma

residueTrans_algebraMap

L50 ↗
AlgebraicGeometry.SubalgebraStages.residueTrans_algebraMap
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueTrans_algebraMap {i j : ι} (h : i ≤ j) (a : S i) :
    residueTrans S p h (algebraMap (S i) (residuePrime S p i).ResidueField a) =
      algebraMap (S j) (residuePrime S p j).ResidueField
        (Subalgebra.inclusion (S.mono h) a)
lemma

residueLeg_algebraMap

L57 ↗
AlgebraicGeometry.SubalgebraStages.residueLeg_algebraMap
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueLeg_algebraMap (i : ι) (a : S i) :
    residueLeg S p i (algebraMap (S i) (residuePrime S p i).ResidueField a) =
      algebraMap A p.ResidueField (a : A)
theorem

residueLeg_injective

L63 ↗
AlgebraicGeometry.SubalgebraStages.residueLeg_injective
Documentation

Each stage residue field embeds in the original residue field.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
theorem residueLeg_injective (i : ι) : Function.Injective (residueLeg S p i)
lemma

residueTrans_refl

L67 ↗
AlgebraicGeometry.SubalgebraStages.residueTrans_refl
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueTrans_refl (i : ι) : residueTrans S p (le_refl i) = RingHom.id _
lemma

residueTrans_comp

L73 ↗
AlgebraicGeometry.SubalgebraStages.residueTrans_comp
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueTrans_comp {i j k : ι} (h : i ≤ j) (h' : j ≤ k) :
    (residueTrans S p h').comp (residueTrans S p h) = residueTrans S p (h.trans h')
lemma

residueLeg_trans

L80 ↗
AlgebraicGeometry.SubalgebraStages.residueLeg_trans
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
lemma residueLeg_trans {i j : ι} (h : i ≤ j) :
    (residueLeg S p j).comp (residueTrans S p h) = residueLeg S p i
def

residueDiagram

L88 ↗
AlgebraicGeometry.SubalgebraStages.residueDiagram
Documentation

The diagram of the actual residue fields at the contracted stage primes.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueDiagram : ι ⥤ CommRingCat.{u} where
  obj i := CommRingCat.of (residuePrime S p i).ResidueField
  map h := CommRingCat.ofHom (residueTrans S p h.le)
  map_id i := CommRingCat.hom_ext (residueTrans_refl S p i)
  map_comp h h' := CommRingCat.hom_ext (residueTrans_comp S p h.le h'.le).symm
def

residueCocone

L95 ↗
AlgebraicGeometry.SubalgebraStages.residueCocone
Documentation

The cocone of actual residue-field embeddings with vertex the ambient residue field.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · full declaration
def residueCocone : Cocone (residueDiagram S p) where
  pt := CommRingCat.of p.ResidueField
  ι :=
    { app i := CommRingCat.ofHom (residueLeg S p i)
      naturality i j h := by
        apply CommRingCat.hom_ext
        exact residueLeg_trans S p h.le }
theorem

exists_residueLeg_eq

L104 ↗
AlgebraicGeometry.SubalgebraStages.exists_residueLeg_eq
Documentation

A residue-field fraction is represented at a stage containing its numerator and denominator.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
theorem exists_residueLeg_eq [IsDirected ι (· ≤ ·)]
    (hS : ∀ a : A, ∃ i, a ∈ S i) (x : p.ResidueField) :
    ∃ (i : ι) (y : (residuePrime S p i).ResidueField), residueLeg S p i y = x
def

residueCoconeIsColimit

L118 ↗
AlgebraicGeometry.SubalgebraStages.residueCoconeIsColimit
Documentation

The actual ambient residue field is the colimit of the contracted stage residue fields.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.SubalgebraStages
universe u
variable {A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable (p : Ideal A) [p.IsPrime]
Lean source · statement
def residueCoconeIsColimit [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (hS : ∀ a : A, ∃ i, a ∈ S i) : IsColimit (residueCocone S p)

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