OAI/AlgebraicGeometry/Seshadri/Sheaves/CartierTensor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.Tensor.tmul_injective_of_local_coefficient line 20
  2. def OAI.MaximalSeshadri.Geometry.frameCoefficient line 47
  3. lemma OAI.MaximalSeshadri.Geometry.frameCoefficient_injective line 65
  4. theorem OAI.MaximalSeshadri.Geometry.LineBundle.tmul_injective line 84
  5. def OAI.MaximalSeshadri.Geometry.sectionMultiplyPresheaf line 118
  6. lemma OAI.MaximalSeshadri.Geometry.sectionMultiplyPresheaf_apply line 126
  7. def OAI.MaximalSeshadri.Geometry.sectionMultiply line 131
  8. lemma OAI.MaximalSeshadri.Geometry.sectionMultiplyPresheaf_mono line 138
  9. theorem OAI.MaximalSeshadri.Geometry.sectionMultiply_mono line 161
  10. def OAI.MaximalSeshadri.Geometry.cartierQuotient line 184
  11. theorem OAI.MaximalSeshadri.Geometry.cartierSequence_exact line 187
  12. theorem OAI.MaximalSeshadri.Geometry.globalCartierDivision line 194