OAI/Geometry/Anticanonical/CanonicalBundle.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Canonical bundles as alternating top forms and their one-dimensional model.

  1. def OAI.CanonicalBundle.altCoordinates line 19
  2. theorem OAI.CanonicalBundle.altCoordinates_injective line 24
  3. instance OAI.CanonicalBundle.altFiniteDimensional line 31
  4. theorem OAI.CanonicalBundle.contMDiffOn_alt line 39
  5. theorem OAI.CanonicalBundle.contMDiffOn_clm line 55
  6. theorem OAI.CanonicalBundle.contMDiffAt_alt line 78
  7. theorem OAI.CanonicalBundle.contMDiffAt_clm line 93
  8. theorem OAI.CanonicalBundle.contMDiffOn_altCoordChange line 138
  9. instance OAI.CanonicalBundle.altVectorPrebundle_isContMDiff line 161
  10. instance OAI.CanonicalBundle.altContMDiffVectorBundle line 169
  11. abbrev OAI.CanonicalBundle.Model line 180
  12. abbrev OAI.CanonicalBundle.Fiber line 183
  13. theorem OAI.CanonicalBundle.canonical_isAnalytic line 186
  14. theorem OAI.CanonicalBundle.canonical_finiteDimensional line 191
  15. def OAI.CanonicalBundle.detForm line 195
  16. def OAI.CanonicalBundle.modelScalarEquiv line 208
  17. theorem OAI.CanonicalBundle.canonical_rank_one line 220