OAI/AlgebraicGeometry/NumericalDimension/FiniteCurveMaps.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Finite Curve Maps.

  1. theorem OAI.NumericalDimensionOne.isClosed_point_of_curve_coheight line 18
  2. theorem OAI.NumericalDimensionOne.finite_closed_of_curve_coheight line 43
  3. theorem OAI.NumericalDimensionOne.finite_of_proper_dominant_from_smooth_curve line 61
  4. theorem OAI.NumericalDimensionOne.normalCurveAffine_isDedekind line 110
  5. def OAI.NumericalDimensionOne.smoothCurvePrimeMap line 148
  6. def OAI.NumericalDimensionOne.smoothCurvePrimeFiberEquiv line 153
  7. lemma OAI.NumericalDimensionOne.divisorSection_dominant_pullback line 179
  8. theorem OAI.NumericalDimensionOne.dominant_sections_linear_injection line 214
  9. theorem OAI.NumericalDimensionOne.dvr_ordFrac_map line 253
  10. def OAI.NumericalDimensionOne.curveRamificationLength line 304
  11. theorem OAI.NumericalDimensionOne.order_dominant_at_prime line 310
  12. theorem OAI.NumericalDimensionOne.cartierPullback_coefficient_ramification line 322
  13. theorem OAI.NumericalDimensionOne.curveRamificationLength_eq_affine line 339
  14. def OAI.NumericalDimensionOne.curveFieldDegree line 394
  15. theorem OAI.NumericalDimensionOne.curveFieldDegree_eq_affine line 398
  16. theorem OAI.NumericalDimensionOne.affineResidue_isAlgClosed line 434
  17. theorem OAI.NumericalDimensionOne.smoothCurve_fiber_ramification_sum line 461
  18. lemma OAI.NumericalDimensionOne.complexWeilDegree_eq_finsum line 514
  19. theorem OAI.NumericalDimensionOne.smoothCurve_degree_cartierPullback line 527
  20. theorem OAI.NumericalDimensionOne.IsPulledCartierRepresentative.comp_dominant line 566