OAI/AlgebraicGeometry/NumericalDimension/ExceptionalFibers.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Exceptional Fibers.

  1. theorem OAI.NumericalDimensionOne.smooth_proper_curve_through_point_avoiding line 20
  2. theorem OAI.NumericalDimensionOne.dominant_of_nonconstant_to_curve line 65
  3. theorem OAI.NumericalDimensionOne.finite_dominant_of_nonconstant_smooth_curve line 83
  4. theorem OAI.NumericalDimensionOne.finite_curve_through_point line 107
  5. theorem OAI.NumericalDimensionOne.projective_finite_curve_through_point line 162
  6. theorem OAI.NumericalDimensionOne.positive_curve_in_closed_subvariety line 194
  7. theorem OAI.NumericalDimensionOne.height_eq_of_closedImmersion line 262
  8. theorem OAI.NumericalDimensionOne.integral_closed_closure line 286
  9. theorem OAI.NumericalDimensionOne.effective_antinef_irreducible_dichotomy line 312
  10. theorem OAI.NumericalDimensionOne.connected_closed_dichotomy_of_irreducible line 349
  11. theorem OAI.NumericalDimensionOne.effective_antinef_connected_fiber line 396
  12. def OAI.NumericalDimensionOne.qDivisorSupport line 421
  13. lemma OAI.NumericalDimensionOne.CartierMultiple.support_eq line 423
  14. lemma OAI.NumericalDimensionOne.CartierMultiple.divisorSupport_eq line 438
  15. lemma OAI.NumericalDimensionOne.CartierMultiple.coeff_nonneg_iff line 443
  16. lemma OAI.NumericalDimensionOne.CartierMultiple.degree_nonpos_of_qDegree_nonpos line 458
  17. theorem OAI.NumericalDimensionOne.qSurface_negativity_of_antinef line 470
  18. theorem OAI.NumericalDimensionOne.qEffective_antinef_connected_fiber line 493
  19. theorem OAI.NumericalDimensionOne.exceptional_prime_not_quasiFiniteAt line 517
  20. theorem OAI.NumericalDimensionOne.exceptional_fiber_not_isOpen_singleton line 534
  21. lemma OAI.NumericalDimensionOne.nonisolated_irreducible_closed_subset line 553