OAI/AlgebraicGeometry/SectionFields/QCartier.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Rational Cartier divisors, pullback and exact principal presentations.

  1. theorem OAI.RelativeDenominators.ord_one line 19
  2. theorem OAI.RelativeDenominators.ord_inv line 23
  3. theorem OAI.RelativeDenominators.ord_pow line 30
  4. theorem OAI.RelativeDenominators.ord_zpow line 40
  5. theorem OAI.RelativeDenominators.ord_div line 50
  6. theorem OAI.RelativeDenominators.pullback_ord_zero_on line 57
  7. abbrev OAI.RelativeDenominators.RationalWeilDivisor line 72
  8. def OAI.RelativeDenominators.rationalPrincipalDivisor line 75
  9. theorem OAI.RelativeDenominators.rationalPrincipalDivisor_apply line 79
  10. def OAI.RelativeDenominators.IsQCartier line 85
  11. theorem OAI.RelativeDenominators.pullback_local_equations_agree line 94
  12. structure OAI.RelativeDenominators.QCartierData line 138
  13. def OAI.RelativeDenominators.IsQCartier.data line 148
  14. def OAI.RelativeDenominators.QCartierData.pullbackCoeff line 155
  15. theorem OAI.RelativeDenominators.QCartierData.pullbackCoeff_eq_local line 161
  16. theorem OAI.RelativeDenominators.QCartierData.pullbackCoeff_finite_support line 176
  17. def OAI.RelativeDenominators.pullbackQCartier line 205
  18. theorem OAI.RelativeDenominators.pullbackQCartier_apply_of_local line 215
  19. theorem OAI.RelativeDenominators.isQCartier_pullback line 227
  20. theorem OAI.RelativeDenominators.ord_pullback_eq_zero_of_mapsToGeneric line 246
  21. def OAI.RelativeDenominators.IsVerticalRationalDivisor line 260
  22. theorem OAI.RelativeDenominators.isVertical_pullbackQCartier line 264
  23. theorem OAI.RelativeDenominators.isQCartier_principal line 276
  24. theorem OAI.RelativeDenominators.pullbackQCartier_principal line 282
  25. theorem OAI.RelativeDenominators.isQCartier_add line 294
  26. theorem OAI.RelativeDenominators.isQCartier_smul line 311
  27. theorem OAI.RelativeDenominators.pullbackQCartier_add line 329
  28. theorem OAI.RelativeDenominators.pullbackQCartier_smul line 372
  29. theorem OAI.RelativeDenominators.rationalPrincipalDivisor_mul line 408
  30. theorem OAI.RelativeDenominators.rationalPrincipalDivisor_div line 415
  31. theorem OAI.RelativeDenominators.rationalPrincipalDivisor_pow line 422
  32. theorem OAI.RelativeDenominators.exact_presentation_of_vertical_principalization line 432
  33. def OAI.RelativeDenominators.RationallyLinearlyEquivalent line 500
  34. theorem OAI.RelativeDenominators.relative_exact_presentation_of_vertical_principalization line 507
  35. theorem OAI.RelativeDenominators.principalDivisor_div line 528
  36. theorem OAI.RelativeDenominators.principalDivisor_constant line 537
  37. theorem OAI.RelativeDenominators.invariant_rescaling_of_conjugate_divisor_eq line 550