AlgebraicGeometry.Scheme.Modules.ProjPresentation.exists_finiteBySections_pullback_of_quasiFiniteAt
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.ProjPresentation
universe u
section gamma_solution
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
attribute [local instance] MvPolynomial.gradedAlgebraLean source · statement
theorem exists_finiteBySections_pullback_of_quasiFiniteAt
{R : Type u} [CommRing R] {X : Scheme.{u}} {f : X ⟶ Spec (.of R)} [IsProper f] {M : X.Modules}
{N : ℕ}
(𝔔 : M.ProjPresentation f N) (𝔭 : PrimeSpectrum R)
(hqf : ∀ x : X, f x = 𝔭 → 𝔔.toProj.QuasiFiniteAt x) :
∃ g : R, g ∉ 𝔭.asIdeal ∧
∀ (A : Type u) [CommRing A] [Algebra R A], IsUnit (algebraMap R A g) →
∀ {X' : Scheme.{u}} (p : X' ⟶ X) (f' : X' ⟶ Spec (.of A)),
IsPullback p f' f (Spec.map (CommRingCat.ofHom (algebraMap R A))) →
Scheme.Modules.FiniteBySections ((Scheme.Modules.pullback p).obj M) f'