OAI/Geometry/Anticanonical/Transport.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Dual tensor powers of canonical bundles and pullback under holomorphic local diffeomorphisms.

  1. structure OAI.AnticanonicalTransport.AnalyticBundle line 14
  2. abbrev OAI.AnticanonicalTransport.canonical line 42
  3. abbrev OAI.AnticanonicalTransport.scalar line 48
  4. abbrev OAI.AnticanonicalTransport.hom line 53
  5. def OAI.AnticanonicalTransport.anti line 58
  6. abbrev OAI.AnticanonicalTransport.H0 line 62
  7. theorem OAI.AnticanonicalTransport.anti_rank_one line 66
  8. theorem OAI.AnticanonicalTransport.hom_triv_equiv line 77
  9. theorem OAI.AnticanonicalTransport.canonical_triv_equiv line 97
  10. theorem OAI.AnticanonicalTransport.contMDiffAt_inverseDerivative line 122
  11. def OAI.AnticanonicalTransport.canonicalPush line 157
  12. theorem OAI.AnticanonicalTransport.canonicalPush_inCoordinates line 164
  13. theorem OAI.AnticanonicalTransport.contMDiffAt_canonicalPush line 184
  14. theorem OAI.AnticanonicalTransport.homPull_inCoordinates line 218
  15. def OAI.AnticanonicalTransport.antiPull line 239
  16. theorem OAI.AnticanonicalTransport.contMDiffAt_antiPull line 245
  17. theorem OAI.AnticanonicalTransport.contMDiff_antiPull_section line 278
  18. def OAI.AnticanonicalTransport.pullSection line 298
  19. theorem OAI.AnticanonicalTransport.pullSection_injective line 304
  20. theorem OAI.AnticanonicalTransport.derivativeEquiv_comp line 322
  21. theorem OAI.AnticanonicalTransport.canonicalPush_comp line 332
  22. theorem OAI.AnticanonicalTransport.antiPull_comp line 339
  23. theorem OAI.AnticanonicalTransport.pullSection_comp line 348
  24. theorem OAI.AnticanonicalTransport.pullSection_deck line 360
  25. theorem OAI.AnticanonicalTransport.antiPull_id line 372
  26. theorem OAI.AnticanonicalTransport.pullSection_id line 391
  27. theorem OAI.AnticanonicalTransport.pullSection_inverse line 401
  28. def OAI.AnticanonicalTransport.pullSectionEquiv line 414