AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_of_isQuasicoherent
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.AffineAcyclicity
attribute [-instance] AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
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
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_of_isQuasicoherent
{R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} [IsAffine V] [IsSeparated π]
(F : OModulePresheaf π) (hF : F.IsQuasicoherent) (K : V.OrderedAffineCover) (i : ℕ) :
Subsingleton (F.HSucc K i)