OAI/AlgebraicGeometry/Seshadri/Intersection/IdealProductDegree.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.Geometry.lift_of_local_module_lifts line 18
  2. lemma OAI.MaximalSeshadri.Geometry.ideal_inclusion_lift line 33
  3. lemma OAI.MaximalSeshadri.Geometry.ideal_inclusions_iso line 60
  4. def OAI.MaximalSeshadri.Geometry.finiteTensor line 77
  5. def OAI.MaximalSeshadri.Geometry.finiteTensorInclusion line 82
  6. lemma OAI.MaximalSeshadri.Geometry.finiteTensorInclusion_mono line 88
  7. def OAI.MaximalSeshadri.Geometry.finiteTensorFrame line 98
  8. lemma OAI.MaximalSeshadri.Geometry.finiteTensorInclusion_ideal line 105
  9. lemma OAI.MaximalSeshadri.Geometry.finite_common_frames line 142
  10. lemma OAI.MaximalSeshadri.Geometry.idealSheaf_prod_ideal line 154
  11. lemma OAI.MaximalSeshadri.Geometry.curveDegree_finiteTensor line 162
  12. theorem OAI.MaximalSeshadri.Geometry.PointBlowup.total_ideal_degree line 174