ModuleIntegralFinitePresentationColimit.lean
Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationColimit
5 declarations indexed from sourceView source ↗ Module documentation
Integral algebras as filtered colimits of finite-FP models
The actual small model cocone is jointly surjective for an integral target, by the finite-subset model construction. Equality of two elements in one stage is detected later by coequalizing the two polynomial evaluation maps. The native filtered-colimit criterion for types then proves that the underlying commutative-ring cocone is colimiting.
All stages and the index remain in the base universe. This is the actual ring-local approximation; global relative-Spec approximation is separate.
Declarations
Algebra.FinitePresentationModel.jointly_surjective
DocumentationEvery element of an integral algebra occurs in an actual indexed model.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace Algebra.FinitePresentationModel
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
Algebra.FinitePresentationModel.eventually_equal
DocumentationEquality in the target is detected after one actual transition map. No integrality assumption is needed for this equality assertion.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace Algebra.FinitePresentationModel
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
Algebra.FinitePresentationModel.ringDiagram
DocumentationThe existing model diagram, viewed as a diagram of commutative rings.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace Algebra.FinitePresentationModel
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
variable (R B)
Algebra.FinitePresentationModel.ringCocone
DocumentationThe actual model cocone in commutative rings.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace Algebra.FinitePresentationModel
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
variable (R B)
Algebra.FinitePresentationModel.ringCoconeIsColimit
DocumentationThe small filtered finite-FP model cocone is an actual ring colimit when the target is integral over the base.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits
namespace Algebra.FinitePresentationModel
variable {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
variable (R B)