OAI/NumberTheory/PiExponent/Geometry/LineBundleFrameCocycle.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSeshadri.LineBundleFrameCocycle.frame line 17
  2. abbrev OAI.PiExponentSeshadri.LineBundleFrameCocycle.coeff line 19
  3. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.coeff_restrict line 22
  4. def OAI.PiExponentSeshadri.LineBundleFrameCocycle.transition line 30
  5. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.coeff_change line 34
  6. def OAI.PiExponentSeshadri.LineBundleFrameCocycle.ofFrames line 40
  7. def OAI.PiExponentSeshadri.LineBundleFrameCocycle.toSections line 72
  8. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.chartEquiv_toSections line 87
  9. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.toSections_bijective line 93
  10. def OAI.PiExponentSeshadri.LineBundleFrameCocycle.presheafHom line 106
  11. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.restrict_presheafHom_isIso line 142
  12. lemma OAI.PiExponentSeshadri.LineBundleFrameCocycle.sheafification_presheafHom_isIso line 153
  13. def OAI.PiExponentSeshadri.LineBundleFrameCocycle.isoSheaf line 168