OAI/AlgebraicGeometry/SurfaceCones/ExteriorFunctor.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Functoriality of Kähler exterior algebras and coordinate-change formulas.

  1. def OAI.CanonicalCoordinates.exteriorFunctor line 13
  2. lemma OAI.CanonicalCoordinates.exteriorFunctor_D line 20
  3. lemma OAI.CanonicalCoordinates.exteriorFunctor_smul line 28
  4. lemma OAI.CanonicalCoordinates.volume_swap line 38
  5. lemma OAI.CanonicalCoordinates.volume_reflect line 44
  6. lemma OAI.CanonicalCoordinates.volume_invert line 51
  7. lemma OAI.SourceSymmetry.rootEquiv_base line 77
  8. abbrev OAI.SourceSymmetry.fieldCoord line 85
  9. lemma OAI.SourceSymmetry.fieldCoord_eq line 86
  10. def OAI.SourceSymmetry.rootProduct line 90
  11. lemma OAI.SourceSymmetry.rootProduct_ne_zero line 91
  12. lemma OAI.SourceSymmetry.rootProduct_eq line 93
  13. lemma OAI.SourceSymmetry.rootEquiv_product line 98
  14. lemma OAI.SourceSymmetry.rootSwap_coord line 114
  15. lemma OAI.SourceSymmetry.rootReflect_coord line 116
  16. lemma OAI.SourceSymmetry.rootInvert_x line 119
  17. lemma OAI.SourceSymmetry.rootInvert_y line 121
  18. def OAI.SourceSymmetry.volumeForm line 125
  19. lemma OAI.SourceSymmetry.canonicalForm_eq_product line 129
  20. lemma OAI.SourceSymmetry.rootSwap_volume line 134
  21. lemma OAI.SourceSymmetry.rootReflect_volume line 139
  22. lemma OAI.SourceSymmetry.rootInvert_volume line 144
  23. def OAI.SourceSymmetry.canonicalExteriorModule line 159
  24. lemma OAI.SourceSymmetry.density_coefficient line 167
  25. lemma OAI.SourceSymmetry.rootEquiv_canonical line 173
  26. lemma OAI.SourceSymmetry.rootSwap_canonical line 192
  27. lemma OAI.SourceSymmetry.rootReflect_canonical line 207
  28. lemma OAI.SourceSymmetry.x_eq_root line 222
  29. lemma OAI.SourceSymmetry.rootInvert_canonical line 226
  30. def OAI.SourceSymmetry.canonicalDensity line 241

    Source documentation

    The exact rational density of a frame of K on the chart indexed by t. Its inverse fifth section factor is the same rational form on every chart.

    def canonicalDensity (t : SectionIndex) : ExteriorAlgebra L Ω[L⁄ℂ] :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex

  31. lemma OAI.SourceSymmetry.weight_cancellation line 244
  32. lemma OAI.SourceSymmetry.rootEquiv_density line 249
  33. lemma OAI.SourceSymmetry.rootSwap_density line 270
  34. lemma OAI.SourceSymmetry.rootReflect_density line 279
  35. lemma OAI.SourceSymmetry.rootInvert_density line 288