OAI/AlgebraicGeometry/Seshadri/Sheaves/CartierModule.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.IdealModule.unit line 18
  2. def OAI.MaximalSeshadri.IdealModule.structureMap line 20
  3. lemma OAI.MaximalSeshadri.IdealModule.structureMap_app line 24
  4. def OAI.MaximalSeshadri.IdealModule.idealModule line 27
  5. def OAI.MaximalSeshadri.IdealModule.inclusion line 29
  6. instance OAI.MaximalSeshadri.IdealModule.(instance at line 32) line 32
  7. def OAI.MaximalSeshadri.IdealModule.sectionsKernelIso line 34
  8. lemma OAI.MaximalSeshadri.IdealModule.sectionsKernelIso_inclusion line 43
  9. lemma OAI.MaximalSeshadri.IdealModule.image_eq_kernel line 56
  10. lemma OAI.MaximalSeshadri.IdealModule.image_eq_ideal line 72
  11. def OAI.MaximalSeshadri.IdealModule.closedModule line 83
  12. def OAI.MaximalSeshadri.IdealModule.closedInclusion line 85
  13. lemma OAI.MaximalSeshadri.IdealModule.closed_image line 88
  14. lemma OAI.MaximalSeshadri.IdealModule.isIso_of_affine_app line 92
  15. def OAI.MaximalSeshadri.IdealModule.multiply line 102
  16. lemma OAI.MaximalSeshadri.IdealModule.multiply_app line 118
  17. lemma OAI.MaximalSeshadri.IdealModule.multiply_structure_zero line 121
  18. def OAI.MaximalSeshadri.IdealModule.equationToIdeal line 132
  19. lemma OAI.MaximalSeshadri.IdealModule.equationToIdeal_inclusion line 136
  20. lemma OAI.MaximalSeshadri.IdealModule.equationToIdeal_app line 140
  21. lemma OAI.MaximalSeshadri.IdealModule.isIso_equationToIdeal line 146
  22. def OAI.MaximalSeshadri.IdealModule.sectionFamily line 187
  23. def OAI.MaximalSeshadri.IdealModule.fromSection line 194
  24. lemma OAI.MaximalSeshadri.IdealModule.fromSection_app line 197
  25. lemma OAI.MaximalSeshadri.IdealModule.fromSection_inclusion_app line 201
  26. lemma OAI.MaximalSeshadri.IdealModule.isIso_fromSection line 215
  27. lemma OAI.MaximalSeshadri.IdealModule.regular_map_flat line 252
  28. lemma OAI.MaximalSeshadri.IdealModule.restriction_regular line 261
  29. def OAI.MaximalSeshadri.IdealModule.restrictedInclusion line 268
  30. instance OAI.MaximalSeshadri.IdealModule.restrictedInclusion_mono line 273
  31. lemma OAI.MaximalSeshadri.IdealModule.restrictedInclusion_app line 281
  32. lemma OAI.MaximalSeshadri.IdealModule.restricted_image line 286
  33. lemma OAI.MaximalSeshadri.IdealModule.frame_restriction line 310
  34. def OAI.MaximalSeshadri.IdealModule.frameOnRange line 337
  35. lemma OAI.MaximalSeshadri.IdealPullback.map_top line 353
  36. lemma OAI.MaximalSeshadri.IdealPullback.comap_top line 358
  37. def OAI.MaximalSeshadri.IdealPullback.specIdeal line 381
  38. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_top line 384
  39. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_comap line 389
  40. lemma OAI.MaximalSeshadri.IdealPullback.comap_ι_top line 403
  41. lemma OAI.MaximalSeshadri.IdealPullback.comap_ideal line 411
  42. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_of_local_equations line 441
  43. theorem OAI.MaximalSeshadri.InvertibleLocal.invertible_of_affine_equations line 465