Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ProjectiveStableHom

Projective-stable Hom spaces in a linear category #

This file forms the scalar quotient of a Hom space by the maps which factor through categorical projectives. It records only the one-sided stable Hom spaces and their postcomposition maps needed by the finite-functor-category Auslander--Reiten argument.

source
structure MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective {D : Type u} [CategoryTheory.Category.{v, u} D] {X Y : D} (f : X ⟶ Y) :
Type (max u v)

A morphism factors through a categorical projective object.

  • middle : D
  • projective : CategoryTheory.Projective self.middle
  • left : X ⟶ self.middle
  • right : self.middle ⟶ Y
  • fac : CategoryTheory.CategoryStruct.comp self.left self.right = f
Instances For
    source
    noncomputable def MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective.zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] {X Y : D} :
    FactorsThroughProjective 0

    The zero map factors through the zero object.

    Instances For
      source
      noncomputable def MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective.add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} {f g : X ⟶ Y} (hf : FactorsThroughProjective f) (hg : FactorsThroughProjective g) :
      FactorsThroughProjective (f + g)

      Projective factorizations are closed under addition.

      Instances For
        source
        def MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective.smul {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] {X Y : D} {f : X ⟶ Y} (a : k) (hf : FactorsThroughProjective f) :
        FactorsThroughProjective (a • f)

        Projective factorizations are closed under scalar multiplication.

        Instances For
          source
          def MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective.postcomp {D : Type u} [CategoryTheory.Category.{v, u} D] {X Y Z : D} {f : X ⟶ Y} (hf : FactorsThroughProjective f) (g : Y ⟶ Z) :
          FactorsThroughProjective (CategoryTheory.CategoryStruct.comp f g)

          Postcomposition preserves projective factorization.

          Instances For
            source
            def MagnitudeConjecture.ProjectiveStable.FactorsThroughProjective.precomp {D : Type u} [CategoryTheory.Category.{v, u} D] {W X Y : D} (g : W ⟶ X) {f : X ⟶ Y} (hf : FactorsThroughProjective f) :
            FactorsThroughProjective (CategoryTheory.CategoryStruct.comp g f)

            Precomposition preserves projective factorization.

            Instances For
              source
              def MagnitudeConjecture.ProjectiveStable.factorSubmodule {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X Y : D) :
              Submodule k (X ⟶ Y)

              The linear subspace of morphisms which factor through projectives.

              Instances For
                source
                @[reducible, inline]
                abbrev MagnitudeConjecture.ProjectiveStable.Hom {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X Y : D) :
                Type v

                The projective-stable Hom space.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev MagnitudeConjecture.ProjectiveStable.mk {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} :
                  (X ⟶ Y) →ₗ[k] Hom X Y

                  The class of an ordinary morphism in projective-stable Hom.

                  Instances For
                    source
                    def MagnitudeConjecture.ProjectiveStable.postcomp {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) {Y Z : D} (g : Y ⟶ Z) :
                    Hom X Y →ₗ[k] Hom X Z

                    Postcomposition on projective-stable Hom.

                    Instances For
                      source
                      @[simp]
                      theorem MagnitudeConjecture.ProjectiveStable.postcomp_mk {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) {Y Z : D} (g : Y ⟶ Z) (f : X ⟶ Y) :
                      (postcomp X g) (mk f) = mk (CategoryTheory.CategoryStruct.comp f g)
                      source
                      theorem MagnitudeConjecture.ProjectiveStable.projective_of_id_factorsThroughProjective {D : Type u} [CategoryTheory.Category.{v, u} D] (X : D) (h : FactorsThroughProjective (CategoryTheory.CategoryStruct.id X)) :
                      CategoryTheory.Projective X

                      If the identity factors through a projective, then the object itself is projective.

                      source
                      theorem MagnitudeConjecture.ProjectiveStable.mk_id_ne_zero {k : Type uk} [Field k] {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) (hX : ¬CategoryTheory.Projective X) :
                      mk (CategoryTheory.CategoryStruct.id X) ≠ 0

                      A nonprojective object has a nonzero stable identity class.