theorem
L80 ↗cechFinite_of_isProper
AlgebraicGeometry.OModulePresheaf.cechFinite_of_isProper
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_of_isProper
attribute [-instance] 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
AlgebraicGeometry.ChowDatum.hι_closed AlgebraicGeometry.ChowDatumProj.hιN_closed
AlgebraicGeometry.ChowDatumProj.hp_proper AlgebraicGeometry.ChowDatum.hp_isoU
AlgebraicGeometry.ChowDatum.hp_proper AlgebraicGeometry.ProjSpace.algebraAway
AlgebraicGeometry.ProjSpace.instIsProperProdOverπ AlgebraicGeometry.ChowDatumProj.hp_isoU
AlgebraicGeometry.ProjSpace.isProper_π AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
ProjSpaceCech.GradedModule.H.module ProjSpaceCech.GradedModule.H.addCommGroup
ProjSpaceCech.GradedModule.sec.instAdd ProjSpaceCech.GradedModule.sec.instNeg
ProjSpaceCech.GradedModule.acg ProjSpaceCech.GradedModule.Frac.setoid
ProjSpaceCech.GradedModule.modR ProjSpaceCech.GradedModule.sec.instModule
ProjSpaceCech.GradedModule.sec.instAddCommGroup ProjSpaceCech.GradedModule.sec.instZero
ProjSpaceCech.GradedModule.Presentation.fJ
attribute [-instance] ProjSpaceCech.GradedModule.sec.instSMul ProjSpaceCech.Twist.H.module
ProjSpaceCech.Idx.instFintype ProjSpaceCech.Twist.H.addCommGroup
ProjSpaceCech.Idx.instDecidableEq ProjSpaceCech.Twist.Mon.instDecidableEq
ProjSpaceCech.Twist.cochain.instAddCommGroup ProjSpaceCech.Twist.cochain.instModule
attribute [-simp] 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 AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
AlgebraicGeometry.ChowDatum.mk.injEq ProjSpaceCech.GradedModule.mk.injEq
ProjSpaceCech.GradedModule.mk.sizeOf_spec ProjSpaceCech.GradedModule.Frac.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Presentation.mk.injEq ProjSpaceCech.GradedModule.Frac.mk.injEq
ProjSpaceCech.GradedModule.Presentation.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.shift_toLinearMap ProjSpaceCech.GradedModule.Hom.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.mk.injEq
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace OppositeLean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_of_isProper
{R : Type u} [CommRing R] [IsNoetherianRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
[IsProper π]
(F : OModulePresheaf π) (hc : F.IsCoherent) (hq : F.IsQuasicoherent) (K :
V.OrderedAffineCover) :
F.CechFinite K