OAI/NumberTheory/PiExponent/Geometry/LineBundleTensor.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PiExponentSeshadri.Geometry.LineBundle line 15
  2. def OAI.PiExponentSeshadri.Geometry.moduleTensor line 20
  3. def OAI.PiExponentSeshadri.Geometry.modulePow line 24
  4. def OAI.PiExponentSeshadri.Geometry.structureSheaf line 28
  5. abbrev OAI.PiExponentSeshadri.Geometry.GlobalSections line 30
  6. def OAI.PiExponentSeshadri.Geometry.sectionOpen line 32
  7. def OAI.PiExponentSeshadri.Geometry.LineBundle.IsAmple line 35
  8. def OAI.PiExponentSeshadri.ModulePresheaf.pushforwardCongr line 51
  9. lemma OAI.PiExponentSeshadri.ModulePresheaf.pushforwardCongr_hom_app line 58
  10. def OAI.PiExponentSeshadri.ModulePresheaf.pushforwardNatTrans line 64
  11. lemma OAI.PiExponentSeshadri.ModulePresheaf.pushforwardNatTrans_app_app line 78
  12. def OAI.PiExponentSeshadri.ModulePresheaf.pushforwardPushforwardAdj line 88
  13. def OAI.PiExponentSeshadri.Geometry.modulePresheafRestrict line 121
  14. def OAI.PiExponentSeshadri.Geometry.modulePresheafRestrictAdjunction line 127
  15. def OAI.PiExponentSeshadri.Geometry.moduleSheafificationRestrict line 140
  16. def OAI.PiExponentSeshadri.Geometry.modulePresheafRestrictOpensIso line 159
  17. def OAI.PiExponentSeshadri.Geometry.modulePresheafTensorRestrict line 171
  18. def OAI.PiExponentSeshadri.Geometry.moduleTensorRestrict line 192
  19. def OAI.PiExponentSeshadri.Geometry.moduleTensorIso line 199
  20. def OAI.PiExponentSeshadri.Geometry.moduleTensorUnit line 206
  21. def OAI.PiExponentSeshadri.Geometry.modulePowFrame line 214
  22. def OAI.PiExponentSeshadri.Geometry.LineBundle.pow line 221
  23. def OAI.PiExponentSeshadri.Geometry.moduleTensorMap line 227
  24. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorMap_id line 232
  25. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorMap_comp line 241
  26. instance OAI.PiExponentSeshadri.Geometry.moduleTensorMap_isIso line 251
  27. def OAI.PiExponentSeshadri.Geometry.modulePowMap line 256
  28. lemma OAI.PiExponentSeshadri.Geometry.modulePowMap_id line 261
  29. lemma OAI.PiExponentSeshadri.Geometry.modulePowMap_comp line 269
  30. instance OAI.PiExponentSeshadri.Geometry.modulePowMap_isIso line 279
  31. def OAI.PiExponentSeshadri.Geometry.modulePowFunctor line 285
  32. def OAI.PiExponentSeshadri.Geometry.unitPowerIso line 291
  33. def OAI.PiExponentSeshadri.Geometry.powerSection line 295
  34. lemma OAI.PiExponentSeshadri.Geometry.powerSection_zero line 299
  35. lemma OAI.PiExponentSeshadri.Geometry.powerSection_natural line 304
  36. instance OAI.PiExponentSeshadri.Geometry.powerSection_isIso line 309
  37. def OAI.PiExponentSeshadri.Geometry.moduleTensorRightUnit line 312