Documentation

TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Numerical

Numerical quotients of the Ext-Euler pairing #

The Ext-Euler characteristic descends to a biadditive pairing on the exact Grothendieck groups of two extension-closed subcategories. This file views that pairing as an integer-bilinear map and applies the separate left and right numerical-quotient construction to it.

The two subcategories are deliberately kept independent: the Ext-Euler pairing is generally nonsymmetric, so its left and right radicals can differ. The generic numerical-quotient API supplies the quotient maps, one-sided pairings, functoriality, and the nondegenerate pairing; this file adds the Ext-Euler names and the computation rules needed by its users.

Main definitions #

Main results #

This is the ordinary Ext-Euler specialization in Layer 7 of the Grothendieck-groups, Cartan-maps, and Euler-forms roadmap. The Laurent/sesquilinear specialization belongs after the graded Ext-Euler pairing has descended to graded K₀.

References #

The Ext-Euler construction follows Weibel, An Introduction to Homological Algebra, Sections 2.4--2.7, and its nonsymmetric numerical quotient follows Dancso--Licata, Koszul algebras and flow lattices, Section 3.1. No formalization is copied or vendored here; the two constructions are combined through the existing Tau Ceti APIs.

source
noncomputable def TauCeti.extEulerBilinear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
ExactK0 (ExactStructure.fullSubcategory P hP) →ₗ[ℤ] ExactK0 (ExactStructure.fullSubcategory Q hQ) →ₗ[ℤ] ℤ

The ordinary Ext-Euler pairing on exact Grothendieck groups, regarded as a bilinear map over ℤ so that it can be fed to the numerical-quotient construction.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.extEulerBilinear_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (x : ExactK0 (ExactStructure.fullSubcategory P hP)) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)) :
    ((extEulerBilinear hP hQ h) x) y = ((extEulerPairing hP hQ h) x) y
    source
    @[reducible, inline]
    abbrev TauCeti.ExtEulerLeftNumericalQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
    Type w

    The left numerical quotient of the first exact Grothendieck group for the Ext-Euler pairing.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.ExtEulerRightNumericalQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
      Type w

      The right numerical quotient of the second exact Grothendieck group for the Ext-Euler pairing.

      Equations
      Instances For
        source
        noncomputable def TauCeti.extEulerLeftNumericalQuotientMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
        ExactK0 (ExactStructure.fullSubcategory P hP) →ₗ[ℤ] ExtEulerLeftNumericalQuotient hP hQ h

        The quotient map from the first exact Grothendieck group to its Ext-Euler numerical quotient.

        Equations
        Instances For
          source
          noncomputable def TauCeti.extEulerRightNumericalQuotientMk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
          ExactK0 (ExactStructure.fullSubcategory Q hQ) →ₗ[ℤ] ExtEulerRightNumericalQuotient hP hQ h

          The quotient map from the second exact Grothendieck group to its Ext-Euler numerical quotient.

          Equations
          Instances For
            source
            theorem TauCeti.mem_extEulerLeftRadical_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (x : ExactK0 (ExactStructure.fullSubcategory P hP)) :
            x ∈ leftRadical (extEulerBilinear hP hQ h) ↔ ∀ (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)), ((extEulerPairing hP hQ h) x) y = 0

            The left radical of the Ext-Euler pairing, characterized by vanishing against every class on the right.

            source
            theorem TauCeti.mem_extEulerRightRadical_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)) :
            y ∈ rightRadical (extEulerBilinear hP hQ h) ↔ ∀ (x : ExactK0 (ExactStructure.fullSubcategory P hP)), ((extEulerPairing hP hQ h) x) y = 0

            The right radical of the Ext-Euler pairing, characterized by vanishing against every class on the left.

            source
            noncomputable def TauCeti.extEulerLeftNumericalPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
            ExtEulerLeftNumericalQuotient hP hQ h →ₗ[ℤ] ExactK0 (ExactStructure.fullSubcategory Q hQ) →ₗ[ℤ] ℤ

            The one-sided pairing after quotienting the left exact Grothendieck group.

            Equations
            Instances For
              source
              noncomputable def TauCeti.extEulerRightNumericalPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
              ExactK0 (ExactStructure.fullSubcategory P hP) →ₗ[ℤ] ExtEulerRightNumericalQuotient hP hQ h →ₗ[ℤ] ℤ

              The one-sided pairing after quotienting the right exact Grothendieck group.

              Equations
              Instances For
                source
                noncomputable def TauCeti.extEulerNumericalPairing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
                ExtEulerLeftNumericalQuotient hP hQ h →ₗ[ℤ] ExtEulerRightNumericalQuotient hP hQ h →ₗ[ℤ] ℤ

                The Ext-Euler pairing between both numerical Grothendieck groups.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.extEulerLeftNumericalPairing_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (x : ExactK0 (ExactStructure.fullSubcategory P hP)) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)) :
                  ((extEulerLeftNumericalPairing hP hQ h) ((extEulerLeftNumericalQuotientMk hP hQ h) x)) y = ((extEulerPairing hP hQ h) x) y

                  The left Ext-Euler numerical pairing evaluates on a quotient representative as the descended Ext-Euler pairing.

                  source
                  @[simp]
                  theorem TauCeti.extEulerRightNumericalPairing_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (x : ExactK0 (ExactStructure.fullSubcategory P hP)) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)) :
                  ((extEulerRightNumericalPairing hP hQ h) x) ((extEulerRightNumericalQuotientMk hP hQ h) y) = ((extEulerPairing hP hQ h) x) y

                  The right Ext-Euler numerical pairing evaluates on a quotient representative as the descended Ext-Euler pairing.

                  source
                  @[simp]
                  theorem TauCeti.extEulerNumericalPairing_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (x : ExactK0 (ExactStructure.fullSubcategory P hP)) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)) :
                  ((extEulerNumericalPairing hP hQ h) ((extEulerLeftNumericalQuotientMk hP hQ h) x)) ((extEulerRightNumericalQuotientMk hP hQ h) y) = ((extEulerPairing hP hQ h) x) y

                  The Ext-Euler numerical pairing evaluates on two quotient representatives as the descended Ext-Euler pairing.

                  source
                  theorem TauCeti.extEulerNumericalPairing_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (X : P.FullSubcategory) (Y : Q.FullSubcategory) :
                  ((extEulerNumericalPairing hP hQ h) ((extEulerLeftNumericalQuotientMk hP hQ h) (ExactK0.of X))) ((extEulerRightNumericalQuotientMk hP hQ h) (ExactK0.of Y)) = extEuler k ⋯

                  The Ext-Euler numerical pairing evaluates on classes of objects as the ordinary Ext-Euler characteristic.

                  source
                  theorem TauCeti.extEulerLeftNumericalPairing_separatingLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
                  (extEulerLeftNumericalPairing hP hQ h).SeparatingLeft

                  The left numerical Ext-Euler pairing separates its left argument.

                  source
                  theorem TauCeti.extEulerRightNumericalPairing_separatingRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
                  (extEulerRightNumericalPairing hP hQ h).SeparatingRight

                  The right numerical Ext-Euler pairing separates its right argument.

                  source
                  theorem TauCeti.extEulerNumericalPairing_nondegenerate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) :
                  (extEulerNumericalPairing hP hQ h).Nondegenerate

                  Quotienting by both Ext-Euler radicals makes the ordinary numerical pairing nondegenerate.

                  source
                  theorem TauCeti.extEulerNumericalPairing_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.LocallySmall.{w, v, u} C] {P Q : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hP : (ExactStructure.abelian C).IsExtensionClosed P) (hQ : (ExactStructure.abelian C).IsExtensionClosed Q) (h : IsEulerAdmissibleOn k P Q) (c : ExtEulerLeftNumericalQuotient hP hQ h →ₗ[ℤ] ExtEulerRightNumericalQuotient hP hQ h →ₗ[ℤ] ℤ) (hc : ∀ (x : ExactK0 (ExactStructure.fullSubcategory P hP)) (y : ExactK0 (ExactStructure.fullSubcategory Q hQ)), (c ((extEulerLeftNumericalQuotientMk hP hQ h) x)) ((extEulerRightNumericalQuotientMk hP hQ h) y) = ((extEulerPairing hP hQ h) x) y) :
                  c = extEulerNumericalPairing hP hQ h

                  The Ext-Euler numerical pairing is the unique bilinear pairing whose representative values are the descended Ext-Euler values.