OAI/AlgebraicGeometry/Seshadri/Model.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Geometry.complexProjectiveSpace line 18

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:18 (same declaration text).

2. def OAI.MaximalSeshadri.Geometry.constantsInDegreeZero line 22

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:22 (same declaration text).

3. def OAI.MaximalSeshadri.Geometry.projectiveSpaceToSpec line 31

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:31 (same declaration text).

4. structure OAI.MaximalSeshadri.Geometry.Surface line 38

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:38 (same declaration text).

5. structure OAI.MaximalSeshadri.Geometry.LineBundle line 53

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:53 (same declaration text).

6. def OAI.MaximalSeshadri.Geometry.moduleTensor line 60

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:60 (same declaration text).

7. def OAI.MaximalSeshadri.Geometry.modulePow line 65

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:65 (same declaration text).

8. def OAI.MaximalSeshadri.Geometry.structureSheaf line 70

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:70 (same declaration text).

9. abbrev OAI.MaximalSeshadri.Geometry.GlobalSections line 73

   Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:73 (same declaration text).

10. def OAI.MaximalSeshadri.Geometry.sectionOpen line 77

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:77 (same declaration text).

11. def OAI.MaximalSeshadri.Geometry.LineBundle.IsAmple line 81

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:81 (same declaration text).

12. def OAI.MaximalSeshadri.Geometry.restrictScalar line 97

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:97 (same declaration text).

13. lemma OAI.MaximalSeshadri.Geometry.restrictScalar_naturality line 100

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:100 (same declaration text).

14. def OAI.MaximalSeshadri.Geometry.sheafHomSMul line 107

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:107 (same declaration text).

15. instance OAI.MaximalSeshadri.Geometry.sheafHomModule line 132

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:132 (same declaration text).

16. instance OAI.MaximalSeshadri.Geometry.sheafLinear line 162

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:162 (same declaration text).

17. instance OAI.MaximalSeshadri.Geometry.schemeHasExt line 182

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:182 (same declaration text).

18. def OAI.MaximalSeshadri.Geometry.baseScalars line 186

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:186 (same declaration text).

19. abbrev OAI.MaximalSeshadri.Geometry.cohomology line 195

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:195 (same declaration text).

20. def OAI.MaximalSeshadri.Geometry.cohomologyDimension line 201

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:201 (same declaration text).

21. def OAI.MaximalSeshadri.Geometry.eulerCharacteristic line 209

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:209 (same declaration text).

22. def OAI.MaximalSeshadri.Geometry.selfIntersection line 215

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:215 (same declaration text).

23. structure OAI.MaximalSeshadri.Geometry.IntegralCurve line 222

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:222 (same declaration text).

24. def OAI.MaximalSeshadri.Geometry.curveDegree line 233

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:233 (same declaration text).

25. abbrev OAI.MaximalSeshadri.Geometry.complexBase line 248

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:248 (same declaration text).

26. abbrev OAI.MaximalSeshadri.Geometry.ComplexPoint line 251

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:251 (same declaration text).

27. def OAI.MaximalSeshadri.Geometry.ComplexPoint.image line 255

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:255 (same declaration text).

28. def OAI.MaximalSeshadri.Geometry.surfacePower line 259

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:259 (same declaration text).

29. def OAI.MaximalSeshadri.Geometry.tupleImage line 263

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:263 (same declaration text).

30. def OAI.MaximalSeshadri.Geometry.tupleZariskiTopology line 269

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:269 (same declaration text).

31. def OAI.MaximalSeshadri.Geometry.Configuration line 274

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:274 (same declaration text).

32. instance OAI.MaximalSeshadri.Geometry.configurationTopology line 277

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:277 (same declaration text).

33. def OAI.MaximalSeshadri.Geometry.idealOrder line 287

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:287 (same declaration text).

34. def OAI.MaximalSeshadri.Geometry.curveMultiplicity line 293

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:293 (same declaration text).

35. def OAI.MaximalSeshadri.Geometry.totalMultiplicity line 300

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:300 (same declaration text).

36. def OAI.MaximalSeshadri.Geometry.seshadriConstant line 305

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:305 (same declaration text).

37. def OAI.MaximalSeshadri.Geometry.moduleCurveDegree line 326

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:326 (same declaration text).

38. def OAI.MaximalSeshadri.Geometry.sectionImageIdeal line 334

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:334 (same declaration text).

39. def OAI.MaximalSeshadri.Geometry.PresentsPullbackIdeal line 345

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:345 (same declaration text).

40. def OAI.MaximalSeshadri.Geometry.InvertiblePullbackIdeal line 352

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:352 (same declaration text).

41. def OAI.MaximalSeshadri.Geometry.centreIdeal line 358

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:358 (same declaration text).

42. def OAI.MaximalSeshadri.Geometry.IsBlowup line 364

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:364 (same declaration text).

43. structure OAI.MaximalSeshadri.Geometry.PointBlowup line 371

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:371 (same declaration text).

44. def OAI.MaximalSeshadri.Geometry.PointBlowup.BoundaryNef line 384

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:384 (same declaration text).

45. def OAI.MaximalSeshadri.Geometry.EventualMaximalSeshadri line 394

    Also declared: ComparatorChallenges/MaximalSeshadriConstants.lean:394 (same declaration text).