NYLL
Module

AffineLimit_homIsLFP_of_locallyOfFinitePresentation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.AffineLimit_homIsLFP_of_locallyOfFinitePresentation
1 declaration indexed from sourceView source ↗

Module documentation

Finite-presentation morphisms satisfy the affine-limit factorization property

A locally finitely presented morphism admits factorizations and eventual equalities over the affine inverse systems arising from finitely generated subalgebras.

Imports5
Imported by4

Declarations

theorem

homIsLFP_of_locallyOfFinitePresentation

L36 ↗
AlgebraicGeometry.AffineLimit.homIsLFP_of_locallyOfFinitePresentation
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace AffineLimit_homIsLFP_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.AffineLimit.homIsLFP_of_locallyOfFinitePresentation
    (R : Type u) [CommRing R] {X : Scheme.{u}} (ξ : X ⟶ Spec (CommRingCat.of R))
    [LocallyOfFinitePresentation ξ] : AffineLimit.HomIsLFP ξ

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