Documentation

LeanPool.BrillNoetherGraphs.Bananas.Jacobian.BananaJacobianProposition214

The banana Jacobian presentation #

This closes the kernel calculation in Proposition 2.14. The reduction algorithm supplies a paper-reduced representative modulo the displayed relations, while reduced-coordinate kernel triviality forces that representative to vanish. The first isomorphism theorem then identifies the displayed quotient with the range of the graph-level divisor-class map.

source
theorem Bananas.bananaCoordinateRelations_eq_displayedRelations {g : ℕ} (B : Banana g) :
bananaCoordinateRelations B = bananaDisplayedRelations B

Proposition 2.14, relation-lattice equality. The diagonal and strand-length relations displayed in the paper generate every relation of the banana coordinate map to divisor classes.

source
@[reducible, inline]
abbrev Bananas.bananaCoordinateClassRange {g : ℕ} (B : Banana g) :
AddSubmonoid (CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ⧸ principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B))

The divisor-class image of the banana coordinate map. By the degree-zero surjectivity theorem, this is the graph Jacobian component; using the range here avoids introducing a second, redundant model of that group.

Equations
Instances For
    source
    def Bananas.bananaDisplayedClassRangeHom {g : ℕ} (B : Banana g) :
    (Fin (g + 1) → ℤ) ⧸ bananaDisplayedRelations B →+ ↥(bananaCoordinateClassRange B)

    The displayed-quotient map to the coordinate class range.

    Equations
    Instances For
      source
      theorem Bananas.bananaDisplayedClassRangeHom_bijective {g : ℕ} (B : Banana g) :
      Function.Bijective ⇑(bananaDisplayedClassRangeHom B)
      source
      noncomputable def Bananas.bananaDisplayedQuotientEquivClassRange {g : ℕ} (B : Banana g) :
      (Fin (g + 1) → ℤ) ⧸ bananaDisplayedRelations B ≃+ ↥(bananaCoordinateClassRange B)

      Proposition 2.14, quotient form. Coordinates modulo the paper's displayed lattice are additively isomorphic to the degree-zero divisor-class range of the banana graph.

      Equations
      Instances For
        source
        theorem Bananas.bananaDisplayedQuotientEquivClassRange_mk {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) :
        (bananaDisplayedQuotientEquivClassRange B) ((QuotientAddGroup.mk' (bananaDisplayedRelations B)) a) = ⟨(bananaCoordinateClassHom B) a, ⋯⟩