Isolating a representable summand in a covering pullback

For a Hom-finite linear category, coefficient-dual corepresentables retain the local endomorphism rings of their representing objects. This permits the finite-support local-ring argument which isolates one dual-corepresentable from an isomorphism between fixed-fibre direct sums.

theorem MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModule_end_isLocalRing {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hlocal : IsLocalRing (CategoryTheory.End X)) : IsLocalRing (CategoryTheory.End (linearCoyonedaLinearModule X))

A covariant linear representable has local endomorphism ring when its representing object does.

@[simp]

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaHomEquiv_functor_map_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y : Cᵒᵖ} (f : X ⟶ Y) (phi : ↑((dualLinearYonedaLinearModuleFunctor.obj X).obj.obj (Opposite.unop Y))) : ((dualLinearYonedaHomEquiv (dualLinearYonedaLinearModuleFunctor.obj X) (Opposite.unop Y)) (dualLinearYonedaLinearModuleFunctor.map f)) phi = (have this := phi; this) f.unop

Evaluation at the identity exposes the representing morphism underlying the dual-corepresentable functor map.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModuleFunctor_faithful {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : dualLinearYonedaLinearModuleFunctor.Faithful

The dual-corepresentable functor is faithful over a field.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModuleFunctor_full {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) : dualLinearYonedaLinearModuleFunctor.Full

Hom-finiteness makes the dual-corepresentable functor full by finite-dimensional double duality.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModule_end_isLocalRing {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (X : C) (hlocal : IsLocalRing (CategoryTheory.End X)) : IsLocalRing (CategoryTheory.End (dualLinearYonedaLinearModule X))

A dual linear corepresentable has local endomorphism ring when the category is Hom-finite and its representing object has local endomorphism ring.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModule_indecomposable {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hfinite : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (X : C) (hlocal : IsLocalRing (CategoryTheory.End X)) : CategoryTheory.Indecomposable (dualLinearYonedaLinearModule X)

Under the same hypotheses, a dual linear corepresentable is indecomposable.

theorem MagnitudeConjecture.LinearCovering.exists_dualCorepresentable_iso_of_fiberSumIso {k : Type u} [Field k] {C D : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Category.{u, 0} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] {X Z : D} (P : Fiber F X) (e : sourceFiberRepresentableLinearModule F X ≅ targetFiberDualCorepresentableLinearModule F Z) (hfinite : ∀ (Y W : C), FiniteDimensional k (Y ⟶ W)) (hlocal : ∀ (Y : C), IsLocalRing (CategoryTheory.End Y)) : ∃ (J : Fiber F Z), Nonempty (CoveringHom.linearCoyonedaLinearModule ↑P ≅ CoveringHom.dualLinearYonedaLinearModule ↑J)

If the fixed-source representable sum is isomorphic to a fixed-target sum of dual corepresentables, a chosen local source summand is isomorphic to one target summand. Finiteness comes from the support of the image of the source identity.