All.lean
Nyll.SchemeTheory.Cohomology.Sheaves.All
0 declarations indexed from sourceView source ↗
Module documentation
General scheme-theoretic foundations and their direct child modules.
Imports28
- Nyll.SchemeTheory.Cohomology.Sheaves.CoherentBaseChange
- Nyll.SchemeTheory.Cohomology.Sheaves.DoubleComplex
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafConstructions
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafHom
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafIdealFiltration
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafLerayBicomplex
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafLerayDoubleComplex
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_AffSES_exists_connectingHom
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_dV_comp_biAug
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_exists_chowSES
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_exists_hom_relHPresheaf_zero
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_isCoherent_relHPresheaf_chow
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_isQuasicoherent_relHPresheaf_chow
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_nonempty_E2I_equiv
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_nonempty_HTot_equiv
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_rows_exact
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_supportedIn_relHPresheaf_chow
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_d_comp_d
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_exists_basicOpen_sections_free_of_isIntegral
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_exists_d_eq_d_of_forall_d_mem_pow_of_isProper
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_exists_idealPowSub_eq_bot
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_hasDevissageStep
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isCoherent_coker
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isCoherent_idealPowQuot
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_coker
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_isQuasicoherent_idealPowQuot
- Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_supportedIn_idealPowQuot
Imported by1
This module has no indexed declarations. Its imports and full source are available here.