AlgebraicGeometry.ProjSpace.exists_isClosedImmersion_isPullback_comp_eq_map
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isClosedImmersion_isPullback_comp_eq_map
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebraLean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_isClosedImmersion_isPullback_comp_eq_map
{A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
(ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
(B : Type u) [CommRing B] [Algebra A B] :
∃ (Z' : Scheme.{u}) (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B))
(_ : IsClosedImmersion ι') (e : Z' ⟶ Z),
IsPullback e (ι' ≫ ProjSpace.π B n) (ι ≫ ProjSpace.π A n) (Spec.map (CommRingCat.ofHom
(algebraMap A B))) ∧
e ≫ ι = ι' ≫ ProjSpace.map A B n