OAI/AlgebraicGeometry/NumericalDimension/GenericMembers.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Generic Members.

  1. lemma OAI.NumericalDimensionOne.smooth_at_generic_fiber line 20
  2. theorem OAI.NumericalDimensionOne.proper_generic_smooth_open line 55
  3. lemma OAI.NumericalDimensionOne.smooth_morphismRestrict_of_preimage_le line 85
  4. theorem OAI.NumericalDimensionOne.exists_smooth_closed_fiber line 104
  5. theorem OAI.NumericalDimensionOne.exists_smooth_closed_fiber_in_open line 152
  6. theorem OAI.NumericalDimensionOne.exists_smooth_incidence_member line 204
  7. lemma OAI.NumericalDimensionOne.idealSheaf_comap_ofIdealTop_affine line 245
  8. def OAI.NumericalDimensionOne.parameterSection line 288
  9. lemma OAI.NumericalDimensionOne.parameterSection_over line 292
  10. lemma OAI.NumericalDimensionOne.parameterSection_map line 296
  11. theorem OAI.NumericalDimensionOne.isPullback_parameterSection line 308
  12. theorem OAI.NumericalDimensionOne.smooth_parameter_member line 315
  13. theorem OAI.NumericalDimensionOne.DivisorAffineAtlas.incidence_exists line 349
  14. theorem OAI.NumericalDimensionOne.DivisorAffineAtlas.exists_smooth_incidence line 358
  15. lemma OAI.NumericalDimensionOne.appTop_ne_zero_of_range_basicOpen line 388
  16. theorem OAI.NumericalDimensionOne.generic_mem_linear_parameter_open line 397
  17. def OAI.NumericalDimensionOne.parameterCoefficient line 431
  18. def OAI.NumericalDimensionOne.parameterLinearCombination line 435
  19. lemma OAI.NumericalDimensionOne.parameter_evaluate_linear line 439
  20. def OAI.NumericalDimensionOne.linearMemberSection line 468
  21. lemma OAI.NumericalDimensionOne.parameterSection_app_universal line 471
  22. lemma OAI.NumericalDimensionOne.parameterSection_naturality line 480
  23. theorem OAI.NumericalDimensionOne.parameter_member_chart line 493
  24. theorem OAI.NumericalDimensionOne.DivisorAffineAtlas.exists_nonzero_smooth_member line 518
  25. lemma OAI.NumericalDimensionOne.open_scalar_topIso line 564
  26. def OAI.NumericalDimensionOne.DivisorProjectiveChart.member line 578
  27. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.member_topIso line 581
  28. theorem OAI.NumericalDimensionOne.DivisorProjectiveChart.member_generic line 588
  29. lemma OAI.NumericalDimensionOne.DivisorProjectiveChart.nonvanishing_section_order line 621
  30. theorem OAI.NumericalDimensionOne.DivisorProjectiveChart.member_divisor_order line 632
  31. theorem OAI.NumericalDimensionOne.smooth_ideal_open_comap line 640