AlgebraicGeometry.ProjSpace.finite_H0_twist_and_finite_HSucc_twist_of_isClosedImmersion
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_finite_H0_twist_and_finite_HSucc_twist_of_isClosedImmersion
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.biC_abGrp
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_smul
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_smul
AlgebraicGeometry.OModulePresheaf.Leray.biC_module
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx DoubleComplex.instModuleE₂I
DoubleComplex.Bounded.modR DoubleComplex.instModuleE₂II DoubleComplex.instAddCommGroupE₂II
DoubleComplex.Bounded.abGrp DoubleComplex.instAddCommGroupE₂I
attribute [-simp] AlgebraicGeometry.OModulePresheaf.prod_obj
AlgebraicGeometry.OModulePresheaf.restrOpen_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
AlgebraicGeometry.OModulePresheaf.sndHom_app AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
AlgebraicGeometry.OModulePresheaf.Hom.id_app
AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
AlgebraicGeometry.OModulePresheaf.AffHom.id_app
AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
AlgebraicGeometry.OModulePresheaf.Leray.restrictToPreimage_U
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U DoubleComplex.Bounded.mk.injEq
DoubleComplex.Bounded.mk.sizeOf_spec DoubleComplex.Convergence.mk.injEq
DoubleComplex.Convergence.mk.sizeOf_spec DoubleComplex.SubQuot.mk.sizeOf_spec
DoubleComplex.SubQuot.mk.injEq
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebraLean source · statement
theorem
_root_.AlgebraicGeometry.ProjSpace.finite_H0_twist_and_finite_HSucc_twist_of_isClosedImmersion
{A : Type u} [CommRing A] [IsNoetherianRing A] {n : ℕ} {Z : Scheme.{u}}
(ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι] (d :
ℕ) :
Module.Finite A ((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).H0 (ProjSpace.stdCoverPullback ι))
∧
(∀ i : ℕ, Module.Finite A ((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).HSucc
(ProjSpace.stdCoverPullback ι) i))