OAI/AlgebraicGeometry/SurfaceCones/DeterminantTransport.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Transport of determinant images under function-field automorphisms and compatible affine-ring isomorphisms.

  1. def OAI.CanonicalCoordinates.rationalExteriorLinear line 17
  2. lemma OAI.CanonicalCoordinates.rationalExteriorLinear_wedge line 29
  3. lemma OAI.CanonicalCoordinates.determinantImage_transport line 35
  4. lemma OAI.CanonicalCoordinates.determinantImage_transport_frame line 56
  5. lemma OAI.SourceSymmetry.swapChart_coe line 83
  6. lemma OAI.SourceSymmetry.reflectChart_coe line 85
  7. lemma OAI.SourceSymmetry.invertChart_coe line 87
  8. lemma OAI.SourceSymmetry.canonicalImage_step line 90
  9. lemma OAI.SourceSymmetry.canonicalImage_word line 105
  10. lemma OAI.SourceSymmetry.canonicalImage_congr line 115
  11. lemma OAI.SourceSymmetry.coefficientChart_canonicalImage line 125

    Source documentation

    The top differential image is the weight-five line lattice on every member of the smooth affine cover.

    lemma coefficientChart_canonicalImage (t : SectionIndex) (ht : Good t) :
    LinearMap.range (determinantMap ℂ (coefficientChart t) L) =
      Submodule.span (coefficientChart t) {canonicalDensity t} := by
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientChart, OAI.SourceSymmetry.canonicalDensity

  12. lemma OAI.CanonicalCoordinates.exterior_projective line 142
  13. lemma OAI.CanonicalCoordinates.zero_baseChange line 159
  14. def OAI.CanonicalCoordinates.exteriorBaseChange line 164
  15. lemma OAI.CanonicalCoordinates.exteriorBaseChange_ι line 172
  16. def OAI.CanonicalCoordinates.baseChangedExteriorMap line 192
  17. lemma OAI.CanonicalCoordinates.baseChangedExteriorMap_injective line 198
  18. lemma OAI.CanonicalCoordinates.exteriorMap_factorization line 205
  19. lemma OAI.CanonicalCoordinates.exteriorMap_injective line 223
  20. lemma OAI.CanonicalCoordinates.determinantMap_injective line 229
  21. def OAI.CanonicalCoordinates.determinantTrivialization line 250
  22. lemma OAI.CanonicalCoordinates.determinantTrivialization_spec line 254
  23. lemma OAI.CanonicalCoordinates.determinantTrivialization_symm_spec line 260
  24. def OAI.CanonicalCoordinates.selfModule line 273
  25. theorem OAI.CanonicalCoordinates.subalgebraDomain line 274
  26. theorem OAI.CanonicalCoordinates.subalgebraTower line 276
  27. theorem OAI.CanonicalCoordinates.subalgebraFaithful line 278
  28. def OAI.SourceSymmetry.coefficientCanonicalFrame line 305

    Source documentation

    A frame of the top cotangent module on every good affine open.

    def coefficientCanonicalFrame (t : SectionIndex) (ht : Good t) :
    (⋀[coefficientChart t]^2 Ω[coefficientChart t⁄ℂ]) ≃ₗ[coefficientChart t]
      coefficientChart t := by
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientChart

  29. lemma OAI.SourceSymmetry.coefficientCanonicalFrame_spec line 312
  30. def OAI.SourceSymmetry.coefficientCanonicalGenerator line 321

    Source documentation

    A generator of the top differential module.

    def coefficientCanonicalGenerator (t : SectionIndex) (ht : Good t) :
    ⋀[coefficientChart t]^2 Ω[coefficientChart t⁄ℂ] :=
…

    Mentions: OAI.SourceSymmetry.SectionIndex, OAI.SourceSymmetry.Good, OAI.SourceSymmetry.coefficientChart

  31. lemma OAI.SourceSymmetry.coefficientCanonicalGenerator_spec line 325
  32. lemma OAI.SourceSymmetry.coefficientCanonicalGenerator_transition line 331