Module

IntegralFinitePresentationDiagram.lean

Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationDiagram

11 declarations indexed from sourceView source ↗

Module documentation

A small filtered diagram of finite, finitely presented algebra models

The objects use the existing FGAlgCatSkeleton, whose presentation data already lies in the base universe. Each object is an actual finite, finitely presented algebra equipped with a map to the target algebra. Morphisms and the diagram are inherited from the native over category.

Common stages use the existing tensor-product universal maps. Parallel arrows are coequalized by the actual finite relation quotient. Thus the index is filtered without assuming any colimit comparison. For an integral target, proving that the displayed cocone is a colimit is the next step.

Imports12

Nyll.SchemeTheory.RingTheory.FinitePresentationCoequalizer
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Algebra.Category.CommAlgCat.FiniteType
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Filtered.Basic
Mathlib.CategoryTheory.InducedCategory
Mathlib.CategoryTheory.Limits.Cones
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.FiniteStability
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

structure

FinitePresentationModelData

L47 ↗

Algebra.FinitePresentationModelData

Documentation

Small presentation data for one finite-FP algebra model over B.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

structure FinitePresentationModelData : Type u where
  /-- The finitely generated algebra presentation representing the model. -/
  presentation : FGAlgCatSkeleton R
  /-- The represented algebra is finite over the base ring. -/
  finite : Module.Finite R presentation.eval.obj
  /-- The represented algebra is finitely presented over the base ring. -/
  finitePresentation : Algebra.FinitePresentation R presentation.eval.obj
  /-- The base-algebra map from the represented model to the ambient algebra. -/
  map : presentation.eval.obj →ₐ[R] B

def

toOver

L58 ↗

Algebra.FinitePresentationModelData.toOver

Documentation

The actual arrow represented by a small model.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

def FinitePresentationModelData.toOver (M : FinitePresentationModelData R B) :
    Over (CommAlgCat.of R B)

abbrev

FinitePresentationModel

L64 ↗

Algebra.FinitePresentationModel

Documentation

The model category has object type Type u and inherits its morphisms from the ordinary over category.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]

Lean source · statement

abbrev FinitePresentationModel : Type u

abbrev

stage

L73 ↗

Algebra.FinitePresentationModel.stage

Documentation

The represented finite-FP algebra.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · statement

abbrev stage (M : FinitePresentationModel R B) : CommAlgCat.{u} R

abbrev

toOver

L77 ↗

Algebra.FinitePresentationModel.toOver

Documentation

A model as its actual arrow to the target algebra.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · statement

abbrev toOver (M : FinitePresentationModel R B) : Over (CommAlgCat.of R B)

theorem

exists_representation

L81 ↗

Algebra.FinitePresentationModel.exists_representation

Documentation

Every actual finite-FP stage has a representative in the small model category.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · statement

theorem exists_representation (A : CommAlgCat.{u} R)
    [Module.Finite R A] [Algebra.FinitePresentation R A] (φ : A →ₐ[R] B) :
    ∃ M : FinitePresentationModel R B,
      Nonempty (Over.mk (CommAlgCat.ofHom φ) ≅ M.toOver)

theorem

common_stage

L96 ↗

Algebra.FinitePresentationModel.common_stage

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · statement

theorem common_stage (M N : FinitePresentationModel R B) :
    ∃ (K : FinitePresentationModel R B) (_ : M ⟶ K) (_ : N ⟶ K), True

theorem

coequalize

L122 ↗

Algebra.FinitePresentationModel.coequalize

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · statement

theorem coequalize {M N : FinitePresentationModel R B} (f g : M ⟶ N) :
    ∃ (K : FinitePresentationModel R B) (h : N ⟶ K), f ≫ h = g ≫ h

instance

(anonymous instance)

L153 ↗

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}

Lean source · full declaration

instance : IsFiltered (FinitePresentationModel R B) where
  cocone_objs := common_stage
  cocone_maps := fun {_ _} f g => coequalize f g
  nonempty := by
    obtain ⟨M, _⟩ := exists_representation (CommAlgCat.of R R) (Algebra.ofId R B)
    exact ⟨M⟩

def

diagram

L163 ↗

Algebra.FinitePresentationModel.diagram

Documentation

The actual small filtered algebra diagram.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}
variable (R B)

Lean source · statement

def diagram : FinitePresentationModel R B ⥤ CommAlgCat.{u} R

def

cocone

L168 ↗

Algebra.FinitePresentationModel.cocone

Documentation

The canonical cocone given by the model maps to B.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits
open scoped TensorProduct
namespace Algebra
variable (R B : Type u) [CommRing R] [CommRing B] [Algebra R B]
namespace FinitePresentationModel
variable {R B}
variable (R B)

Lean source · full declaration

def cocone : Cocone (diagram R B) where
  pt := CommAlgCat.of R B
  ι :=
    { app := fun M => CommAlgCat.ofHom M.map
      naturality := fun _ _ f =>
        (Over.w f.hom).trans (Category.comp_id _).symm }

Module documentation

A small filtered diagram of finite, finitely presented algebra models

Declarations