Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FGModuleCatAdditiveFinrank

Finrank under additive functors of finite-dimensional vector spaces #

Every finite-dimensional vector space is a finite biproduct of copies of the ground field. Consequently an additive endofunctor of FGModuleCat k multiplies finrank by its value on the one-dimensional object. This is the small categorical calculation used to extend the string-detector delta formula from coefficient space k to every finite coefficient space.

source
noncomputable def MagnitudeConjecture.FiniteVectorSpace.biproductLinearEquivPi {k : Type u} [Field k] {n : ℕ} (V : Fin n → FGModuleCat k) :
↑(⨁ V) ≃ₗ[k] (i : Fin n) → ↑(V i)

The underlying space of a finite biproduct is linearly equivalent to the ordinary dependent product of the underlying spaces.

Instances For
    source
    theorem MagnitudeConjecture.FiniteVectorSpace.finrank_biproduct {k : Type u} [Field k] {n : ℕ} (V : Fin n → FGModuleCat k) :
    Module.finrank k ↑(⨁ V) = ∑ i : Fin n, Module.finrank k ↑(V i)

    Finrank is additive on a finite biproduct of finite-dimensional vector spaces.

    source
    noncomputable def MagnitudeConjecture.FiniteVectorSpace.biproductLinearEquivPiSameUniverse {k : Type u} [Field k] {ι : Type u} [Fintype ι] (V : ι → FGModuleCat k) :
    ↑(⨁ V) ≃ₗ[k] (i : ι) → ↑(V i)

    The same finrank formula for an index type in the ambient universe.

    Instances For
      source
      theorem MagnitudeConjecture.FiniteVectorSpace.finrank_biproduct_sameUniverse {k : Type u} [Field k] {ι : Type u} [Fintype ι] (V : ι → FGModuleCat k) :
      Module.finrank k ↑(⨁ V) = ∑ i : ι, Module.finrank k ↑(V i)

      Finrank is additive on a finite biproduct indexed in the ambient universe.

      source
      noncomputable def MagnitudeConjecture.FiniteVectorSpace.isoBiproductUnit {k : Type u} [Field k] (V : FGModuleCat k) :
      V ≅ ⨁ fun (x : Fin (Module.finrank k ↑V)) => FGModuleCat.of k k

      A finite-dimensional vector space is isomorphic to the finite biproduct of finrank copies of the ground field.

      Instances For
        source
        theorem MagnitudeConjecture.FiniteVectorSpace.finrank_map_eq_mul {k : Type u} [Field k] (F : CategoryTheory.Functor (FGModuleCat k) (FGModuleCat k)) [F.Additive] (V : FGModuleCat k) :
        Module.finrank k ↑(F.obj V) = Module.finrank k ↑V * Module.finrank k ↑(F.obj (FGModuleCat.of k k))

        An additive endofunctor of finite-dimensional vector spaces scales finrank by the finrank of its value on the ground field.