OAI/AlgebraicGeometry/StableCoordinate/BundleCharts.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Algebra of the two charts of the determinant bundle

This module formalizes the quadric-to-determinant-ring map in Section 4 of the source. All variables are independent before taking the displayed principal-ideal quotient. The chosen sections over D(z+1) and D(z) prove the base map injective without assuming that the quadric ring is a domain.

  1. def OAI.StableCoordinate.BundleCharts.quadricIdeal line 23

    Source documentation

    Defining ideal of the quadric with independent coordinates (x,y,z,u).

    def quadricIdeal : Ideal (MvPolynomial (Fin 4) K) :=
…
  2. abbrev OAI.StableCoordinate.BundleCharts.QuadricRing line 27

    Source documentation

    Coordinate ring of the quadric times the affine u-line.

    abbrev QuadricRing := MvPolynomial (Fin 4) K ⧸ quadricIdeal K

    Mentions: OAI.StableCoordinate.BundleCharts.quadricIdeal

  3. def OAI.StableCoordinate.BundleCharts.determinantIdeal line 30

    Source documentation

    Defining ideal of the determinant-one ring with coordinates (a,d,b,c,u).

    def determinantIdeal : Ideal (MvPolynomial (Fin 5) K) :=
…
  4. abbrev OAI.StableCoordinate.BundleCharts.DeterminantRing line 34

    Source documentation

    Coordinate ring of SL₂ × A¹, in the source's coordinate order.

    abbrev DeterminantRing := MvPolynomial (Fin 5) K ⧸ determinantIdeal K

    Mentions: OAI.StableCoordinate.BundleCharts.determinantIdeal

  5. def OAI.StableCoordinate.BundleCharts.qgen line 37

    Source documentation

    The four quotient generators (x,y,z,u).

    def qgen (i : Fin 4) : QuadricRing K := Ideal.Quotient.mk _ (X i)

    Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing

  6. def OAI.StableCoordinate.BundleCharts.dgen line 40

    Source documentation

    The five quotient generators (a,d,b,c,u).

    def dgen (i : Fin 5) : DeterminantRing K := Ideal.Quotient.mk _ (X i)

    Mentions: OAI.StableCoordinate.BundleCharts.DeterminantRing

  7. theorem OAI.StableCoordinate.BundleCharts.quadric_relation line 42
  8. theorem OAI.StableCoordinate.BundleCharts.determinant_relation line 50
  9. def OAI.StableCoordinate.BundleCharts.basePolynomialMap line 59

    Source documentation

    The map of polynomial rings underlying x=ab, y=dc, z=db, u=u.

    def basePolynomialMap : MvPolynomial (Fin 4) K →ₐ[K] DeterminantRing K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.DeterminantRing

  10. theorem OAI.StableCoordinate.BundleCharts.quadricIdeal_le_ker_basePolynomialMap line 63
  11. def OAI.StableCoordinate.BundleCharts.baseMap line 73

    Source documentation

    The source's quadric-to-determinant-ring map.

    def baseMap : QuadricRing K →ₐ[K] DeterminantRing K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.DeterminantRing

  12. theorem OAI.StableCoordinate.BundleCharts.baseMap_qgen line 77
  13. abbrev OAI.StableCoordinate.BundleCharts.ChartA line 85

    Source documentation

    The base chart D(z+1).

    abbrev ChartA := Localization.Away (qgen K 2 + 1)

    Mentions: OAI.StableCoordinate.BundleCharts.qgen

  14. abbrev OAI.StableCoordinate.BundleCharts.ChartD line 88

    Source documentation

    The base chart D(z).

    abbrev ChartD := Localization.Away (qgen K 2)

    Mentions: OAI.StableCoordinate.BundleCharts.qgen

  15. def OAI.StableCoordinate.BundleCharts.agen line 91

    Source documentation

    Base-chart coordinate functions.

    def agen (i : Fin 4) : ChartA K := algebraMap (QuadricRing K) _ (qgen K i)

    Mentions: OAI.StableCoordinate.BundleCharts.ChartA, OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.qgen

  16. def OAI.StableCoordinate.BundleCharts.zgen line 94

    Source documentation

    Base-chart coordinate functions.

    def zgen (i : Fin 4) : ChartD K := algebraMap (QuadricRing K) _ (qgen K i)

    Mentions: OAI.StableCoordinate.BundleCharts.ChartD, OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.qgen

  17. def OAI.StableCoordinate.BundleCharts.ainv line 97

    Source documentation

    Inverse of z+1 on the first chart.

    def ainv : ChartA K := IsLocalization.Away.invSelf (qgen K 2 + 1)

    Mentions: OAI.StableCoordinate.BundleCharts.ChartA, OAI.StableCoordinate.BundleCharts.qgen

  18. def OAI.StableCoordinate.BundleCharts.zinv line 100

    Source documentation

    Inverse of z on the second chart.

    def zinv : ChartD K := IsLocalization.Away.invSelf (qgen K 2)

    Mentions: OAI.StableCoordinate.BundleCharts.ChartD, OAI.StableCoordinate.BundleCharts.qgen

  19. theorem OAI.StableCoordinate.BundleCharts.agen_relation line 102
  20. theorem OAI.StableCoordinate.BundleCharts.zgen_relation line 106
  21. theorem OAI.StableCoordinate.BundleCharts.agen_mul_ainv line 110
  22. theorem OAI.StableCoordinate.BundleCharts.zgen_mul_zinv line 114
  23. def OAI.StableCoordinate.BundleCharts.sectionAPolynomialMap line 118

    Source documentation

    The section with a=1 over D(z+1), expressed on polynomial generators.

    def sectionAPolynomialMap : MvPolynomial (Fin 5) K →ₐ[K] ChartA K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.ChartA

  24. def OAI.StableCoordinate.BundleCharts.sectionDPolynomialMap line 122

    Source documentation

    The section with d=1 over D(z), expressed on polynomial generators.

    def sectionDPolynomialMap : MvPolynomial (Fin 5) K →ₐ[K] ChartD K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.ChartD

  25. theorem OAI.StableCoordinate.BundleCharts.determinantIdeal_le_ker_sectionAPolynomialMap line 125
  26. theorem OAI.StableCoordinate.BundleCharts.determinantIdeal_le_ker_sectionDPolynomialMap line 136
  27. def OAI.StableCoordinate.BundleCharts.sectionA line 148

    Source documentation

    Restriction to the section a=1 of the determinant bundle on the first base chart.

    def sectionA : DeterminantRing K →ₐ[K] ChartA K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.DeterminantRing, OAI.StableCoordinate.BundleCharts.ChartA

  28. def OAI.StableCoordinate.BundleCharts.sectionD line 153

    Source documentation

    Restriction to the section d=1 of the determinant bundle on the second base chart.

    def sectionD : DeterminantRing K →ₐ[K] ChartD K :=
…

    Mentions: OAI.StableCoordinate.BundleCharts.DeterminantRing, OAI.StableCoordinate.BundleCharts.ChartD

  29. theorem OAI.StableCoordinate.BundleCharts.sectionA_dgen line 157
  30. theorem OAI.StableCoordinate.BundleCharts.sectionD_dgen line 163
  31. theorem OAI.StableCoordinate.BundleCharts.sectionA_y line 169
  32. theorem OAI.StableCoordinate.BundleCharts.sectionA_z line 173
  33. theorem OAI.StableCoordinate.BundleCharts.sectionD_x line 176
  34. theorem OAI.StableCoordinate.BundleCharts.sectionA_comp_baseMap line 180

    Source documentation

    The first local section splits the base map after localization.

    theorem sectionA_comp_baseMap :
    (sectionA K).comp (baseMap K) = IsScalarTower.toAlgHom K (QuadricRing K) (ChartA K) := by
…

    Mentions: OAI.StableCoordinate.BundleCharts.sectionA, OAI.StableCoordinate.BundleCharts.baseMap, OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.ChartA

  35. theorem OAI.StableCoordinate.BundleCharts.sectionD_comp_baseMap line 189

    Source documentation

    The second local section splits the base map after localization.

    theorem sectionD_comp_baseMap :
    (sectionD K).comp (baseMap K) = IsScalarTower.toAlgHom K (QuadricRing K) (ChartD K) := by
…

    Mentions: OAI.StableCoordinate.BundleCharts.sectionD, OAI.StableCoordinate.BundleCharts.baseMap, OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.ChartD

  36. theorem OAI.StableCoordinate.BundleCharts.sectionA_baseMap line 197
  37. theorem OAI.StableCoordinate.BundleCharts.sectionD_baseMap line 201
  38. theorem OAI.StableCoordinate.BundleCharts.eq_zero_of_chartA_eq_zero_of_chartD_eq_zero line 207

    Source documentation

    The two principal opens cover the base: vanishing on both localizations forces zero. This argument works over an arbitrary commutative coefficient ring, without a domain assumption.

    theorem eq_zero_of_chartA_eq_zero_of_chartD_eq_zero (p : QuadricRing K)
    (hA : algebraMap (QuadricRing K) (ChartA K) p = 0)
    (hD : algebraMap (QuadricRing K) (ChartD K) p = 0) : p = 0 := by
…

    Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.ChartA, OAI.StableCoordinate.BundleCharts.ChartD

  39. theorem OAI.StableCoordinate.BundleCharts.baseMap_eq_zero line 224

    Source documentation

    The base map has zero kernel, proved using the two explicit local sections.

    theorem baseMap_eq_zero (p : QuadricRing K) (hp : baseMap K p = 0) : p = 0 := by
…

    Mentions: OAI.StableCoordinate.BundleCharts.QuadricRing, OAI.StableCoordinate.BundleCharts.baseMap

  40. theorem OAI.StableCoordinate.BundleCharts.baseMap_injective line 230

    Source documentation

    The quadric-to-determinant-ring map of Section 4 is injective.

    theorem baseMap_injective : Function.Injective (baseMap K) := by
…

    Mentions: OAI.StableCoordinate.BundleCharts.baseMap