AlgebraicGeometry.Scheme.Modules.exists_projPresentation_isPullback_toProj_of_faithfullyFlat
A projective presentation descends through a faithfully flat base change.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace AlgebraicGeometry.Scheme.ModulesLean source · statement
theorem exists_projPresentation_isPullback_toProj_of_faithfullyFlat
{S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S'] [Module.FaithfullyFlat S
S']
{X X' : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of S)) [QuasiCompact f] [IsSeparated f]
(f' : X' ⟶ Spec (CommRingCat.of S')) (c : X' ⟶ X)
(hc : IsPullback c f' f (Spec.map (CommRingCat.ofHom (algebraMap S S'))))
(L : X.Modules) (hL : Scheme.Modules.IsInvertible L) (L' : X'.Modules)
(e : (Scheme.Modules.pullback c).obj L ≅ L')
{M : ℕ} (𝔔 : Scheme.Modules.ProjPresentation L' f' M) :
∃ (N : ℕ) (𝔓 : Scheme.Modules.ProjPresentation L f N) (𝔓' : Scheme.Modules.ProjPresentation L'
f' N),
IsPullback c 𝔓'.toProj 𝔓.toProj (ProjSpace.map S S' N) ∧
∀ j : Fin (M + 1), ∃ a : Fin (N + 1) → S',
𝔔.σ j = ∑ l, ((f'.appLE ⊤ ⊤ le_top).hom ((Scheme.ΓSpecIso (CommRingCat.of S')).inv.hom (a
l))) • 𝔓'.σ l