Indecomposable modules are supported on one orthogonal block

noncomputable def MagnitudeConjecture.CoveringHom.orthogonalBlockProjection {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (j : J) : CategoryTheory.End M

The natural projection of a module onto one orthogonal block.

theorem MagnitudeConjecture.CoveringHom.orthogonalBlockProjection_idempotent {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (j : J) : IsIdempotentElem (orthogonalBlockProjection block hcross M j)

A block projection is an idempotent endomorphism.

theorem MagnitudeConjecture.CoveringHom.exists_nonzero_fiber_of_indecomposable {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : ∃ (X : C), ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)

An indecomposable finite module is nonzero at some base object.

theorem MagnitudeConjecture.CoveringHom.orthogonalBlockProjection_eq_id {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (X : C) (hX : ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)) : orthogonalBlockProjection block hcross M (block X) = CategoryTheory.CategoryStruct.id M

A projection containing a nonzero fiber of an indecomposable is the identity.

theorem MagnitudeConjecture.CoveringHom.isZero_fiber_of_block_ne {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (X : C) (hX : ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)) (Y : C) (hYX : block Y ≠ block X) : CategoryTheory.Limits.IsZero (M.obj.obj.obj Y)

A module indecomposable has zero fibers outside the block of any nonzero fiber.

theorem MagnitudeConjecture.CoveringHom.existsUnique_support_block {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : ∃! j : J, ∀ (X : C), block X ≠ j → CategoryTheory.Limits.IsZero (M.obj.obj.obj X)

Exactly one orthogonal block supports an indecomposable finite module.

theorem MagnitudeConjecture.CoveringHom.nonzero_map_has_nonzero_fibers {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M N : FiniteDimensionalModuleCategory k) (f : N ⟶ M) (hf : f ≠ 0) : ∃ (X : C), ¬CategoryTheory.Limits.IsZero (N.obj.obj.obj X) ∧ ¬CategoryTheory.Limits.IsZero (M.obj.obj.obj X)

A nonzero module map is nonzero at some object, where both fibers are nonzero.

theorem MagnitudeConjecture.CoveringHom.incoming_source_supported_on_block {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type w} (block : C → J) (hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0) (M : FiniteDimensionalModuleCategory k) (j : J) (hM : ∀ (X : C), block X ≠ j → CategoryTheory.Limits.IsZero (M.obj.obj.obj X)) (N : FiniteDimensionalModuleCategory k) (hN : CategoryTheory.Indecomposable N) (f : N ⟶ M) (hf : f ≠ 0) (Y : C) : block Y ≠ j → CategoryTheory.Limits.IsZero (N.obj.obj.obj Y)

Every indecomposable mapping nontrivially into a block-supported module is supported on that same block.