OAI/Geometry/Anticanonical/Product.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Product decompositions of canonical bundles and naturality of anticanonical sections.

  1. abbrev OAI.CanonicalProduct.scalarEquiv line 17
  2. def OAI.CanonicalProduct.productForm line 23
  3. theorem OAI.CanonicalProduct.scalarEquiv_congr line 28
  4. theorem OAI.CanonicalProduct.productForm_natural line 41
  5. def OAI.CanonicalProduct.productOperator line 58
  6. theorem OAI.CanonicalProduct.productOperator_apply line 63
  7. def OAI.CanonicalProduct.productEquiv line 69
  8. theorem OAI.CanonicalProduct.productEquiv_apply line 78
  9. theorem OAI.CanonicalProduct.productEquiv_coe line 83
  10. theorem OAI.CanonicalProduct.tangent_triv_prod line 103
  11. theorem OAI.CanonicalProduct.canonical_product_coords line 138
  12. def OAI.CanonicalProduct.frameInsert line 160
  13. theorem OAI.CanonicalProduct.frameInsert_inCoordinates line 168
  14. theorem OAI.CanonicalProduct.contMDiffAt_frameInsert line 198
  15. theorem OAI.CanonicalProduct.product_homPull_inCoordinates line 232
  16. def OAI.CanonicalProduct.antiSplit line 254
  17. theorem OAI.CanonicalProduct.contMDiffAt_antiSplit line 264
  18. theorem OAI.CanonicalProduct.contMDiff_antiSplit_apply line 302
  19. theorem OAI.CanonicalProduct.derivativeEquiv_prod line 341
  20. theorem OAI.CanonicalProduct.canonicalPush_product line 353
  21. theorem OAI.CanonicalProduct.frameInsert_natural line 368
  22. theorem OAI.CanonicalProduct.antiSplit_natural line 377