Magnitude conjecture

MagnitudeConjecture.CategoryTheory.OrthogonalMatrixBlocks

Endomorphism algebras of mutually orthogonal finite blocks #

source
@[reducible, inline]
abbrev MagnitudeConjecture.CategoryTheory.blockMatrixTuple {C : Type u} {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) :
CategoryTheory.Mat_ C

All objects in the block family, as one finite matrix object.

Instances For
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.CategoryTheory.blockMatrixTupleAt {C : Type u} {J I : Type} [Fintype I] (X : J → I → C) (j : J) :
    CategoryTheory.Mat_ C

    The finite matrix object belonging to a single block.

    Instances For
      source
      def MagnitudeConjecture.CategoryTheory.blockDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) (f : CategoryTheory.End (blockMatrixTuple X)) (j : J) :
      CategoryTheory.End (blockMatrixTupleAt X j)

      Extract the endomorphism matrix on one diagonal block.

      Instances For
        source
        theorem MagnitudeConjecture.CategoryTheory.blockDiagonal_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) (hzero : ∀ (j l : J), j ≠ l → ∀ (i t : I) (f : X j i ⟶ X l t), f = 0) (f g : CategoryTheory.End (blockMatrixTuple X)) (j : J) :
        blockDiagonal X (CategoryTheory.CategoryStruct.comp f g) j = CategoryTheory.CategoryStruct.comp (blockDiagonal X f j) (blockDiagonal X g j)

        Orthogonality makes restriction to a diagonal block preserve composition.

        source
        def MagnitudeConjecture.CategoryTheory.blockDiagonalAlgHom {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) (hzero : ∀ (j l : J), j ≠ l → ∀ (i t : I) (f : X j i ⟶ X l t), f = 0) :
        CategoryTheory.End (blockMatrixTuple X) →ₐ[k] (j : J) → CategoryTheory.End (blockMatrixTupleAt X j)

        Restriction to the diagonal blocks is an algebra homomorphism.

        Instances For
          source
          theorem MagnitudeConjecture.CategoryTheory.blockDiagonal_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) (hzero : ∀ (j l : J), j ≠ l → ∀ (i t : I) (f : X j i ⟶ X l t), f = 0) :
          Function.Injective (blockDiagonal X)

          Every endomorphism is determined by its diagonal blocks.

          source
          theorem MagnitudeConjecture.CategoryTheory.blockDiagonal_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) :
          Function.Surjective (blockDiagonal X)

          Any family of block endomorphisms extends to the full matrix object.

          source
          noncomputable def MagnitudeConjecture.CategoryTheory.orthogonalBlockEndAlgEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J I : Type} [Fintype J] [Fintype I] (X : J → I → C) (hzero : ∀ (j l : J), j ≠ l → ∀ (i t : I) (f : X j i ⟶ X l t), f = 0) :
          CategoryTheory.End (blockMatrixTuple X) ≃ₐ[k] (j : J) → CategoryTheory.End (blockMatrixTupleAt X j)

          Mutually orthogonal blocks split the endomorphism algebra as a product.

          Instances For