OAI/AlgebraicGeometry/Seshadri/Sheaves/Frames.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Frames.O line 16
  2. def OAI.MaximalSeshadri.Frames.endValue line 18
  3. lemma OAI.MaximalSeshadri.Frames.end_apply line 20
  4. lemma OAI.MaximalSeshadri.Frames.endValue_id line 26
  5. lemma OAI.MaximalSeshadri.Frames.endValue_comp line 28
  6. def OAI.MaximalSeshadri.Frames.frameChange line 32
  7. def OAI.MaximalSeshadri.Frames.coefficient line 38
  8. lemma OAI.MaximalSeshadri.Frames.coefficient_change line 41
  9. lemma OAI.MaximalSeshadri.Frames.coefficient_frame line 47
  10. def OAI.MaximalSeshadri.Frames.restrictSection line 50
  11. def OAI.MaximalSeshadri.Frames.restrictFrame line 54
  12. lemma OAI.MaximalSeshadri.Frames.end_naturality line 58
  13. lemma OAI.MaximalSeshadri.Frames.endValue_restrict line 67
  14. lemma OAI.MaximalSeshadri.Frames.coefficient_restrict line 86
  15. lemma OAI.MaximalSeshadri.Frames.restrictUnit_comp line 105
  16. lemma OAI.MaximalSeshadri.Frames.restrictSection_comp line 123
  17. lemma OAI.MaximalSeshadri.Frames.coefficient_transport line 146
  18. lemma OAI.MaximalSeshadri.Frames.coefficient_restrict_comp line 150
  19. lemma OAI.MaximalSeshadri.Frames.restrictSection_congr line 160
  20. lemma OAI.MaximalSeshadri.Frames.overlap_coefficients line 171
  21. def OAI.MaximalSeshadri.Frames.scalarEnd line 207
  22. lemma OAI.MaximalSeshadri.Frames.endValue_scalarEnd line 223
  23. lemma OAI.MaximalSeshadri.Frames.endValue_injective line 227
  24. lemma OAI.MaximalSeshadri.Frames.end_isIso_iff line 235
  25. lemma OAI.MaximalSeshadri.Frames.coefficient_isUnit_iff line 251