Documentation

AxiomaticGW.Tautological.Getzler

Getzler's relation on Mbar(1,4) #

Getzler's relation is represented as a named relation generator. The seven terms use Getzler's orbifold-cycle normalization; an encoding into decorated strata must therefore provide the normalization explicitly. Vanishing in the known-relations quotient is formal, while validity in a geometric cohomology target remains a separately visible hypothesis.

source
inductive AxiomaticGW.GetzlerStratum :
Type

The seven symmetric codimension-two cycles occurring in Getzler's relation on Mbar(1,4).

Instances For
    source
    @[implicit_reducible]
    instance AxiomaticGW.instDecidableEqGetzlerStratum :
    DecidableEq GetzlerStratum
    Equations
    source
    @[implicit_reducible]
    instance AxiomaticGW.instFintypeGetzlerStratum :
    Fintype GetzlerStratum

    The finite index has seven relation terms. It is distinct from Fin 4, which labels the four marked points of Mbar(1,4).

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[simp]
    theorem AxiomaticGW.getzlerStratum_card :
    Fintype.card GetzlerStratum = 7
    source
    def AxiomaticGW.GetzlerStratum.coefficient :
    GetzlerStratum → ℚ

    Coefficient of a named cycle in Getzler's relation `12 delta22 - 4 delta23 - 2 delta24 + 6 delta34 + delta03 + delta04

    • 2 deltaBeta`.
    Equations
    Instances For
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta22 :
      delta22.coefficient = 12
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta23 :
      delta23.coefficient = -4
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta24 :
      delta24.coefficient = -2
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta34 :
      delta34.coefficient = 6
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta03 :
      delta03.coefficient = 1
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_delta04 :
      delta04.coefficient = 1
      source
      @[simp]
      theorem AxiomaticGW.GetzlerStratum.coefficient_deltaBeta :
      deltaBeta.coefficient = -2
      source
      structure AxiomaticGW.GetzlerStrataEncoding :
      Type

      A concrete encoding of Getzler's seven named orbifold cycles as rational linear combinations of decorated strata. The codimension proof prevents a normalization table from silently referring to the wrong graph type.

      Instances For
        source
        noncomputable def AxiomaticGW.GetzlerStrataEncoding.relation (E : GetzlerStrataEncoding) :
        StrataModule 1 (Fin 4)

        The exact linear combination in Getzler's relation.

        Equations
        Instances For
          source
          theorem AxiomaticGW.GetzlerStrataEncoding.relation_mem_degree (E : GetzlerStrataEncoding) :
          E.relation ∈ StrataModule.degree 2

          Getzler's relation is homogeneous of codimension two.

          source
          noncomputable def AxiomaticGW.GetzlerStrataEncoding.knownRelations (E : GetzlerStrataEncoding) :
          Submodule ℚ (StrataModule 1 (Fin 4))

          Known relations generated by dimension vanishing and the chosen encoding of Getzler's relation. This is a submodule, not a claim of completeness.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev AxiomaticGW.GetzlerStrataEncoding.KnownQuotient (E : GetzlerStrataEncoding) :
            Type

            The module quotient in which the encoded Getzler relation is imposed.

            Equations
            Instances For
              source
              theorem AxiomaticGW.GetzlerStrataEncoding.relation_eq_zero (E : GetzlerStrataEncoding) :
              (StrataModule.quotientMk E.knownRelations) E.relation = 0

              The encoded Getzler combination vanishes in the quotient where it is a named relation generator. This does not prove the geometric relation.

              source
              structure AxiomaticGW.GetzlerRelationGeometry {R : Type u_1} [CommRing R] [Algebra ℚ R] (C : StableCurveCohomology R) :
              Type u_1

              Semantic realization of the seven normalized Getzler cycles in an abstract stable-curve cohomology target.

              Instances For
                source
                theorem AxiomaticGW.GetzlerStrataEncoding.relation_mem_realization_kernel {R : Type u_1} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (E : GetzlerStrataEncoding) (A : StrataRealization C 1 (Fin 4)) (G : GetzlerRelationGeometry C) (hcycle : ∀ (x : GetzlerStratum), A.map (E.cycle x) = G.cycle x) :
                E.relation ∈ A.kernel

                If an encoded cycle realizes as the corresponding geometric cycle, the encoded Getzler combination lies in the realization kernel.

                source
                theorem AxiomaticGW.GetzlerStrataEncoding.knownRelations_le_realization_kernel {R : Type u_1} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (E : GetzlerStrataEncoding) (A : StrataRealization C 1 (Fin 4)) (G : GetzlerRelationGeometry C) (hcycle : ∀ (x : GetzlerStratum), A.map (E.cycle x) = G.cycle x) :
                E.knownRelations ≤ A.kernel

                The dimension and encoded Getzler relations lie in the kernel of every compatible geometric realization.

                source
                noncomputable def AxiomaticGW.GetzlerStrataEncoding.realizationFactor {R : Type u_1} [CommRing R] [Algebra ℚ R] {C : StableCurveCohomology R} (E : GetzlerStrataEncoding) (A : StrataRealization C 1 (Fin 4)) (G : GetzlerRelationGeometry C) (hcycle : ∀ (x : GetzlerStratum), A.map (E.cycle x) = G.cycle x) :
                E.KnownQuotient →ₗ[ℚ] (C.H 1 (Fin 4)).carrier

                Factor a compatible geometric realization through the quotient imposing the encoded Getzler relation and dimension vanishing.

                Equations
                Instances For