OAI/AlgebraicGeometry/Seshadri/Configurations/Configurations.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.affine_pullback_isIntegral line 21
  2. def OAI.MaximalSeshadri.nonemptyAffineCover line 33
  3. instance OAI.MaximalSeshadri.nonemptyAffineCover_nonempty line 49
  4. instance OAI.MaximalSeshadri.nonemptyAffineCover_integral line 54
  5. theorem OAI.MaximalSeshadri.scheme_product_isIntegral line 59
  6. def OAI.MaximalSeshadri.powerSuccIso line 121
  7. def OAI.MaximalSeshadri.overPowerZeroIso line 136
  8. def OAI.MaximalSeshadri.overLeftIso line 146
  9. theorem OAI.MaximalSeshadri.scheme_power_isIntegral line 153
  10. theorem OAI.MaximalSeshadri.scheme_power_locallyOfFiniteType line 172
  11. theorem OAI.MaximalSeshadri.scheme_rational_point_outside_countable_closed line 203
  12. theorem OAI.MaximalSeshadri.rationalPoint_image_injective line 256
  13. abbrev OAI.MaximalSeshadri.RationalPoint line 304
  14. def OAI.MaximalSeshadri.rationalImage line 307
  15. theorem OAI.MaximalSeshadri.rationalImage_injective line 310
  16. def OAI.MaximalSeshadri.rationalTupleImage line 318
  17. lemma OAI.MaximalSeshadri.rationalImage_projection line 322
  18. theorem OAI.MaximalSeshadri.exists_distinct_rational_tuple line 330
  19. def OAI.MaximalSeshadri.pairProjection line 349
  20. def OAI.MaximalSeshadri.pairDiagonal line 354
  21. lemma OAI.MaximalSeshadri.pairDiagonal_closed line 358
  22. lemma OAI.MaximalSeshadri.pairDiagonal_tuple_iff line 363
  23. def OAI.MaximalSeshadri.collisionLocus line 401
  24. lemma OAI.MaximalSeshadri.collisionLocus_closed line 405
  25. lemma OAI.MaximalSeshadri.tuple_not_collision_iff line 409
  26. lemma OAI.MaximalSeshadri.collisionLocus_proper line 423
  27. lemma OAI.MaximalSeshadri.rationalTupleImage_projections line 431
  28. def OAI.MaximalSeshadri.SchemeConfiguration line 441
  29. instance OAI.MaximalSeshadri.schemeConfigurationTopology line 444
  30. theorem OAI.MaximalSeshadri.configuration_outside_countable_closed line 448
  31. instance OAI.MaximalSeshadri.Geometry.complexUncountable line 505
  32. instance OAI.MaximalSeshadri.Geometry.projectiveSpaceToSpec_separated line 511
  33. instance OAI.MaximalSeshadri.Geometry.Surface.separated line 515
  34. lemma OAI.MaximalSeshadri.Geometry.configurationTopology_eq line 519
  35. theorem OAI.MaximalSeshadri.Geometry.surface_configuration_outside_countable_closed line 528