Module

FGSubalgebra_nonempty_isColimit_cocone.lean

Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebra_nonempty_isColimit_cocone

1 declaration indexed from sourceView source ↗

Module documentation

An algebra as a colimit of finitely generated subalgebras

The natural cocone of finitely generated subalgebras presents the original algebra as its colimit in the category of commutative rings.

Imports4

Mathlib.Algebra.Category.Ring.Colimits
Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.CategoryTheory.Limits.Types.Filtered
Nyll.SchemeTheory.Descent.FGSubalgebra

Imported by2

theorem

nonempty_isColimit_cocone

L33 ↗

AlgebraicGeometry.FGSubalgebra.nonempty_isColimit_cocone

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.FGSubalgebra_nonempty_isColimit_cocone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.FGSubalgebra.nonempty_isColimit_cocone
    (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] :
    Nonempty (IsColimit (FGSubalgebra.cocone R A))

Module documentation

An algebra as a colimit of finitely generated subalgebras

Declarations

nonempty_isColimit_cocone