Magnitude conjecture

MagnitudeConjecture.CategoryTheory.LinearBiproduct

Linear Hom spaces and finite biproducts #

Small reusable linear-algebra interfaces for passing between morphisms into a finite biproduct and the family of their components. They are used to turn a chosen Krull--Schmidt middle-term decomposition into the corresponding Hom- dimension sum.

source
noncomputable def MagnitudeConjecture.CategoryTheory.homBiproductLinearEquiv (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (X : C) (F : J → C) :
(X ⟶ ⨁ F) ≃ₗ[k] (j : J) → X ⟶ F j

A morphism into a finite biproduct is linearly equivalent to its family of components.

Instances For
    source
    noncomputable def MagnitudeConjecture.CategoryTheory.homBiproductLinearEquivOfIso (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (X Y : C) (F : J → C) (e : Y ≅ ⨁ F) :
    (X ⟶ Y) ≃ₗ[k] (j : J) → X ⟶ F j

    Transport the component equivalence across an isomorphism with a finite biproduct.

    Instances For
      source
      noncomputable def MagnitudeConjecture.CategoryTheory.biproductHomLinearEquiv (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (Y : C) (F : J → C) :
      (⨁ F ⟶ Y) ≃ₗ[k] (j : J) → F j ⟶ Y

      A morphism from a finite biproduct is linearly equivalent to its family of restrictions to the summands.

      Instances For
        source
        noncomputable def MagnitudeConjecture.CategoryTheory.biproductHomLinearEquivOfIso (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (X Y : C) (F : J → C) (e : X ≅ ⨁ F) :
        (X ⟶ Y) ≃ₗ[k] (j : J) → F j ⟶ Y

        Transport the summand-restriction equivalence across an isomorphism with a finite biproduct.

        Instances For
          source
          theorem MagnitudeConjecture.CategoryTheory.finrank_hom_eq_sum_of_iso_biproduct (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (X Y : C) (F : J → C) (e : Y ≅ ⨁ F) [FiniteDimensional k (X ⟶ Y)] [∀ (j : J), FiniteDimensional k (X ⟶ F j)] :
          Module.finrank k (X ⟶ Y) = ∑ j : J, Module.finrank k (X ⟶ F j)

          Hom dimension into a displayed finite biproduct is the sum of the Hom dimensions into its summands.

          source
          theorem MagnitudeConjecture.CategoryTheory.finrank_hom_eq_sum_of_biproduct_iso (k : Type s) [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (X Y : C) (F : J → C) (e : X ≅ ⨁ F) [FiniteDimensional k (X ⟶ Y)] [∀ (j : J), FiniteDimensional k (F j ⟶ Y)] :
          Module.finrank k (X ⟶ Y) = ∑ j : J, Module.finrank k (F j ⟶ Y)

          Hom dimension from a displayed finite biproduct is the sum of the Hom dimensions from its summands.

          source
          noncomputable def MagnitudeConjecture.CategoryTheory.biproductSplitAtIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] (F : J → C) (i : J) :
          ⨁ F ≅ (⨁ Subtype.restrict (fun (j : J) => j ≠ i) F) ⊞ F i

          Split a selected summand out of a finite biproduct, retaining the remaining summands as a biproduct over the complementary subtype.

          Instances For