ModulesSectionsTensorV2.lean
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesSectionsTensorV2
0 declarations indexed from sourceView source ↗
Module documentation
Modules Sections Tensor V2
Imports4
Imported by9
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_eulerChar_twist_pushforwardUnit_succ_sub_eq_monoidalV2
- Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_exists_polynomial_forall_eulerChar_tensor_tensorPow_eq_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.All
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_bijective_lift_tensorSectionsBilin_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_section_ne_zero_of_dual_section_ne_zero
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_ProjPresentation_exists_linearMap_sections_tensorPow_twistObj_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_bijective_lift_tensorSectionsBilin_of_isQuasicoherent_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_of_pullback_iso_unit_monoidalV2
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_tensorPowSection_smul_monoidalV2
This module has no indexed declarations. Its imports and full source are available here.