Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ProjectivePresentationExt

Degree-one Ext from a short projective presentation #

For a short exact sequence 0 ⟶ K ⟶ P ⟶ X ⟶ 0 with projective middle term, this file identifies Ext¹(X,Y) with the quotient of Hom(K,Y) by maps which extend across P. The equivalence is also proved natural under postcomposition in Y.

source
noncomputable def MagnitudeConjecture.ProjectivePresentationExt.connectingLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) :
(S.X₁ ⟶ Y) →ₗ[k] CategoryTheory.Abelian.Ext S.X₃ Y 1

The connecting map of a short exact sequence, as a linear map.

Instances For
    source
    def MagnitudeConjecture.ProjectivePresentationExt.presentationPrecompLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) :
    (S.X₂ ⟶ Y) →ₗ[k] S.X₁ ⟶ Y

    Precomposition with the first map of a short complex.

    Instances For
      source
      @[reducible, inline]
      abbrev MagnitudeConjecture.ProjectivePresentationExt.presentationRange {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) :
      Submodule k (S.X₁ ⟶ Y)

      The presentation coboundaries.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.ProjectivePresentationExt.mem_presentationRange_iff {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) (Y : C) (f : S.X₁ ⟶ Y) :
        f ∈ presentationRange S Y ↔ ∃ (u : S.X₂ ⟶ Y), CategoryTheory.CategoryStruct.comp S.f u = f
        source
        theorem MagnitudeConjecture.ProjectivePresentationExt.presentationRange_eq_connectingLinear_ker {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) :
        presentationRange S Y = (connectingLinear hS Y).ker

        Exactness identifies presentation coboundaries with the kernel of the connecting map.

        source
        theorem MagnitudeConjecture.ProjectivePresentationExt.connectingLinear_surjective_of_ext_subsingleton_middle {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) [Subsingleton (CategoryTheory.Abelian.Ext S.X₂ Y 1)] :
        Function.Surjective ⇑(connectingLinear hS Y)

        Vanishing of degree-one extensions out of the middle term makes the connecting map surjective.

        source
        theorem MagnitudeConjecture.ProjectivePresentationExt.connectingLinear_surjective {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] (Y : C) :
        Function.Surjective ⇑(connectingLinear hS Y)

        Projectivity of the middle term makes the connecting map surjective.

        source
        noncomputable def MagnitudeConjecture.ProjectivePresentationExt.quotientLinearEquivExtOne {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] (Y : C) :
        ((S.X₁ ⟶ Y) ⧸ presentationRange S Y) ≃ₗ[k] CategoryTheory.Abelian.Ext S.X₃ Y 1

        A short projective presentation computes degree-one Ext.

        Instances For
          source
          @[simp]
          theorem MagnitudeConjecture.ProjectivePresentationExt.quotientLinearEquivExtOne_mk {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] (Y : C) (f : S.X₁ ⟶ Y) :
          (quotientLinearEquivExtOne hS Y) (Submodule.Quotient.mk f) = hS.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯
          source
          def MagnitudeConjecture.ProjectivePresentationExt.postcompQuotient {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) {Y Y' : C} (a : Y ⟶ Y') :
          (S.X₁ ⟶ Y) ⧸ presentationRange S Y →ₗ[k] (S.X₁ ⟶ Y') ⧸ presentationRange S Y'

          Postcomposition descends to the presentation quotient.

          Instances For
            source
            @[simp]
            theorem MagnitudeConjecture.ProjectivePresentationExt.postcompQuotient_mk {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (S : CategoryTheory.ShortComplex C) {Y Y' : C} (a : Y ⟶ Y') (f : S.X₁ ⟶ Y) :
            (postcompQuotient S a) (Submodule.Quotient.mk f) = Submodule.Quotient.mk (CategoryTheory.CategoryStruct.comp f a)
            source
            noncomputable def MagnitudeConjecture.ProjectivePresentationExt.pushforwardLinear {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (S : CategoryTheory.ShortComplex C) {Y Y' : C} (a : Y ⟶ Y') :
            CategoryTheory.Abelian.Ext S.X₃ Y 1 →ₗ[k] CategoryTheory.Abelian.Ext S.X₃ Y' 1

            Pushforward on degree-one Ext.

            Instances For
              source
              theorem MagnitudeConjecture.ProjectivePresentationExt.connectingLinear_postcomp {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y Y' : C} (a : Y ⟶ Y') (f : S.X₁ ⟶ Y) :
              (connectingLinear hS Y') (CategoryTheory.CategoryStruct.comp f a) = (pushforwardLinear S a) ((connectingLinear hS Y) f)

              The connecting map commutes with postcomposition.

              source
              theorem MagnitudeConjecture.ProjectivePresentationExt.quotientLinearEquivExtOne_postcompQuotient {k : Type uk} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] {Y Y' : C} (a : Y ⟶ Y') (q : (S.X₁ ⟶ Y) ⧸ presentationRange S Y) :
              (quotientLinearEquivExtOne hS Y') ((postcompQuotient S a) q) = (pushforwardLinear S a) ((quotientLinearEquivExtOne hS Y) q)

              The quotient description is natural under pushforward.

              source
              def MagnitudeConjecture.ProjectivePresentationExt.presentationToProjectiveStable {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Projective S.X₂] (Y : C) :
              (S.X₁ ⟶ Y) ⧸ presentationRange S Y →ₗ[k] ProjectiveStable.Hom S.X₁ Y

              The presentation quotient maps canonically onto projective-stable Hom: every presentation coboundary factors through the projective middle term.

              Instances For
                source
                @[simp]
                theorem MagnitudeConjecture.ProjectivePresentationExt.presentationToProjectiveStable_mk {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Projective S.X₂] (Y : C) (f : S.X₁ ⟶ Y) :
                (presentationToProjectiveStable Y) (Submodule.Quotient.mk f) = ProjectiveStable.mk f
                source
                theorem MagnitudeConjecture.ProjectivePresentationExt.presentationToProjectiveStable_surjective {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Projective S.X₂] (Y : C) :
                Function.Surjective ⇑(presentationToProjectiveStable Y)

                The canonical map from the presentation quotient onto stable Hom is surjective.

                source
                theorem MagnitudeConjecture.ProjectivePresentationExt.presentationToProjectiveStable_postcompQuotient {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Projective S.X₂] {Y Y' : C} (a : Y ⟶ Y') (q : (S.X₁ ⟶ Y) ⧸ presentationRange S Y) :
                (presentationToProjectiveStable Y') ((postcompQuotient S a) q) = (ProjectiveStable.postcomp S.X₁ a) ((presentationToProjectiveStable Y) q)

                The presentation-to-stable quotient is natural under postcomposition.

                source
                noncomputable def MagnitudeConjecture.ProjectivePresentationExt.extOneToProjectiveStable {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] (Y : C) :
                CategoryTheory.Abelian.Ext S.X₃ Y 1 →ₗ[k] ProjectiveStable.Hom S.X₁ Y

                The canonical quotient from Ext¹(S.X₃,Y) onto projective-stable Hom(S.X₁,Y).

                Instances For
                  source
                  theorem MagnitudeConjecture.ProjectivePresentationExt.extOneToProjectiveStable_surjective {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] (Y : C) :
                  Function.Surjective ⇑(extOneToProjectiveStable hS Y)

                  The canonical map from degree-one Ext onto stable Hom is surjective.

                  source
                  theorem MagnitudeConjecture.ProjectivePresentationExt.extOneToProjectiveStable_postcomp {k : Type uk} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasBinaryBiproducts C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Projective S.X₂] {Y Y' : C} (a : Y ⟶ Y') (xi : CategoryTheory.Abelian.Ext S.X₃ Y 1) :
                  (extOneToProjectiveStable hS Y') ((pushforwardLinear S a) xi) = (ProjectiveStable.postcomp S.X₁ a) ((extOneToProjectiveStable hS Y) xi)

                  The quotient from degree-one Ext to stable Hom is natural under postcomposition.