ModulesPushforwardRestrict.lean
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesPushforwardRestrict
0 declarations indexed from sourceView source ↗
Module documentation
Compatibility import for restriction of module direct images
The original public declarations now live in SchemeTheory.Modules.PushforwardRestrict.
Imported by7
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_exists_isPullback_snd_specMap_algebraOfHom
- Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finiteType_algebraOfHom
- Nyll.AlgebraicCurves.Geometry.Sheaves.All
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_pullback_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_forall_exists_isPullback
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_I_eq_of_lineBundle_iso_tensor_pullback_of_forall_fibre
- Nyll.JacobianVarieties.Picard.relEffCartierDiv_I_eq_of_lineBundle_iso_tensor_pullback_of_supportedIn
This module has no indexed declarations. Its imports and full source are available here.