OAI/AlgebraicGeometry/NumericalDimension/CanonicalChains.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Canonical Chains.

  1. theorem OAI.NumericalDimensionOne.surface_prime_degree_at_stalk_iso line 18
  2. lemma OAI.NumericalDimensionOne.order_dominantFunctionFieldMap_of_stalk_iso line 94
  3. lemma OAI.NumericalDimensionOne.IsCartierPullback.coeff_eq_of_stalk_iso line 121
  4. theorem OAI.NumericalDimensionOne.surfaceIntersection_pullback line 142
  5. lemma OAI.NumericalDimensionOne.rationalTopFormPullback_comp line 214
  6. lemma OAI.NumericalDimensionOne.topDifferentialMap_self line 248
  7. lemma OAI.NumericalDimensionOne.topDifferentialMap_self_of_algebra_eq line 261
  8. lemma OAI.NumericalDimensionOne.rationalTopFormPullback_congr line 268
  9. lemma OAI.NumericalDimensionOne.rationalTopFormPullback_id line 276
  10. lemma OAI.NumericalDimensionOne.rationalTopFormPullback_isIso_injective line 282
  11. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.symm line 302
  12. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.restrictSource line 315
  13. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.restrictTarget line 368
  14. lemma OAI.NumericalDimensionOne.NoExtractionOn.refl line 384
  15. lemma OAI.NumericalDimensionOne.NoExtractionOn.trans line 387
  16. lemma OAI.NumericalDimensionOne.CanonicalMMPChain.noExtraction line 404
  17. lemma OAI.NumericalDimensionOne.CanonicalMMPChain.isOver line 409
  18. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.refl line 425
  19. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.trans' line 429
  20. lemma OAI.NumericalDimensionOne.CompatibleCanonicalData.trans line 471
  21. lemma OAI.NumericalDimensionOne.CanonicalMMPChain.compatible line 479
  22. lemma OAI.NumericalDimensionOne.IsCartierPullback.nsmul line 498
  23. lemma OAI.NumericalDimensionOne.IsQCartierPullback.eq_integral line 505