OAI/AlgebraicGeometry/Seshadri/Sheaves/Restriction.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.ModulePresheaf.pushforwardCongr line 18
  2. lemma OAI.MaximalSeshadri.ModulePresheaf.pushforwardCongr_hom_app line 25
  3. def OAI.MaximalSeshadri.ModulePresheaf.pushforwardNatTrans line 31
  4. lemma OAI.MaximalSeshadri.ModulePresheaf.pushforwardNatTrans_app_app line 45
  5. def OAI.MaximalSeshadri.ModulePresheaf.pushforwardPushforwardAdj line 55
  6. def OAI.MaximalSeshadri.Geometry.modulePresheafRestrict line 86
  7. def OAI.MaximalSeshadri.Geometry.modulePresheafRestrictAdjunction line 92
  8. def OAI.MaximalSeshadri.Geometry.moduleSheafificationRestrict line 105
  9. def OAI.MaximalSeshadri.Geometry.modulePresheafRestrictOpensIso line 125
  10. def OAI.MaximalSeshadri.Geometry.modulePresheafTensorRestrict line 137
  11. def OAI.MaximalSeshadri.Geometry.moduleTensorRestrict line 161
  12. def OAI.MaximalSeshadri.Geometry.moduleTensorIso line 168
  13. def OAI.MaximalSeshadri.Geometry.moduleTensorUnit line 175
  14. def OAI.MaximalSeshadri.Geometry.modulePowFrame line 183
  15. def OAI.MaximalSeshadri.Geometry.LineBundle.pow line 190
  16. def OAI.MaximalSeshadri.Geometry.moduleTensorMap line 205
  17. lemma OAI.MaximalSeshadri.Geometry.moduleTensorMap_id line 210
  18. lemma OAI.MaximalSeshadri.Geometry.moduleTensorMap_comp line 219
  19. instance OAI.MaximalSeshadri.Geometry.moduleTensorMap_isIso line 229
  20. def OAI.MaximalSeshadri.Geometry.modulePowMap line 234
  21. lemma OAI.MaximalSeshadri.Geometry.modulePowMap_id line 239
  22. lemma OAI.MaximalSeshadri.Geometry.modulePowMap_comp line 247
  23. instance OAI.MaximalSeshadri.Geometry.modulePowMap_isIso line 257
  24. def OAI.MaximalSeshadri.Geometry.modulePowFunctor line 263
  25. def OAI.MaximalSeshadri.Geometry.unitPowerIso line 269
  26. def OAI.MaximalSeshadri.Geometry.powerSection line 273
  27. lemma OAI.MaximalSeshadri.Geometry.powerSection_zero line 277
  28. lemma OAI.MaximalSeshadri.Geometry.powerSection_natural line 282
  29. instance OAI.MaximalSeshadri.Geometry.powerSection_isIso line 287
  30. lemma OAI.MaximalSeshadri.Geometry.tensorComparison_natural line 298
  31. lemma OAI.MaximalSeshadri.Geometry.modulePresheafTensorRestrict_natural line 320
  32. lemma OAI.MaximalSeshadri.Geometry.sheafificationComparison_natural line 333
  33. lemma OAI.MaximalSeshadri.Geometry.moduleTensorRestrict_natural line 355
  34. lemma OAI.MaximalSeshadri.Geometry.moduleTensorIso_hom line 382
  35. def OAI.MaximalSeshadri.Geometry.modulePowRestrict line 385
  36. lemma OAI.MaximalSeshadri.Geometry.modulePowRestrict_natural line 391
  37. lemma OAI.MaximalSeshadri.Geometry.modulePowMap_restrict_isIso line 416
  38. lemma OAI.MaximalSeshadri.Geometry.powerSection_restrict_isIso line 428
  39. lemma OAI.MaximalSeshadri.Geometry.sectionOpen_le_powerSection line 437