OAI/AlgebraicGeometry/Seshadri/Intersection/LocalSectionDegree.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Geometry.sectionRestrictionLinear line 18
  2. lemma OAI.MaximalSeshadri.Geometry.sectionRestrictionLinear_surjective line 36
  3. def OAI.MaximalSeshadri.Geometry.restrictCokernelIso line 47
  4. def OAI.MaximalSeshadri.Geometry.moduleIsoTop line 58
  5. lemma OAI.MaximalSeshadri.Geometry.LineBundle.restrict_nonzero line 67
  6. def OAI.MaximalSeshadri.Geometry.sectionQuotientLocalMap line 79
  7. lemma OAI.MaximalSeshadri.Geometry.sectionQuotientLocalMap_surjective line 91
  8. lemma OAI.MaximalSeshadri.Geometry.baseScalars_comp_actual line 104
  9. def OAI.MaximalSeshadri.Geometry.sectionQuotientLocalComplex line 110
  10. theorem OAI.MaximalSeshadri.Geometry.projective_local_section_quotient_finite line 132
  11. theorem OAI.MaximalSeshadri.Geometry.projective_local_section_length_le_degree line 155