Nakayama--Hom duality for finite representable sums

For a covariant linear module M, dual co-Yoneda identifies maps from M to the coefficient-dual corepresentable at X with the coefficient dual of M(X). Combined with linear Yoneda, this is the Nakayama--Hom comparison for a representable projective. The construction here is presentation-level: the later Auslander--Reiten argument only needs finite sums of these literal representables and their representing matrices.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaValueLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : ↑((dualLinearYonedaLinearModule X).obj.obj Y) ≃ₗ[k] Module.Dual k (Y ⟶ X)

The definitional value of a bundled dual corepresentable, exposed as a linear equivalence so that its linear structure can be used without unfolding the full-subcategory wrappers.

@[simp]

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaValueLinearEquiv_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (phi : ↑((dualLinearYonedaLinearModule X).obj.obj Y)) : (dualLinearYonedaValueLinearEquiv X Y) phi = have this := phi; this

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaHomToDualEvaluation {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) : (M ⟶ dualLinearYonedaLinearModule X) →ₗ[k] Module.Dual k ↑(M.obj.obj X)

Evaluation at the identity in the dual co-Yoneda lemma.

noncomputable def MagnitudeConjecture.CoveringHom.dualEvaluationToDualLinearYonedaHom {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) : Module.Dual k ↑(M.obj.obj X) →ₗ[k] M ⟶ dualLinearYonedaLinearModule X

A functional on M(X) determines a natural map from M to the dual corepresentable at X.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaHomEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) : (M ⟶ dualLinearYonedaLinearModule X) ≃ₗ[k] Module.Dual k ↑(M.obj.obj X)

Linear dual co-Yoneda: maps into a dual corepresentable are exactly functionals on the value at its representing object.

noncomputable def MagnitudeConjecture.CoveringHom.representableNakayamaHomEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) : (M ⟶ dualLinearYonedaLinearModule X) ≃ₗ[k] Module.Dual k (linearCoyonedaLinearModule X ⟶ M)

Nakayama--Hom duality for one literal representable projective.

@[simp]

theorem MagnitudeConjecture.CoveringHom.representableNakayamaHomEquiv_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) (X : C) (a : M ⟶ dualLinearYonedaLinearModule X) (f : linearCoyonedaLinearModule X ⟶ M) : ((representableNakayamaHomEquiv M X) a) f = ((dualLinearYonedaValueLinearEquiv X X) ((CategoryTheory.ConcreteCategory.hom (a.hom.app X)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app X)) (CategoryTheory.CategoryStruct.id X)))) (CategoryTheory.CategoryStruct.id X)

theorem MagnitudeConjecture.CoveringHom.representableNakayamaHomEquiv_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : LinearModuleCategory k} (X : C) (g : M ⟶ N) (a : N ⟶ dualLinearYonedaLinearModule X) (f : linearCoyonedaLinearModule X ⟶ M) : ((representableNakayamaHomEquiv M X) (CategoryTheory.CategoryStruct.comp g a)) f = ((representableNakayamaHomEquiv N X) a) (CategoryTheory.CategoryStruct.comp f g)

Naturality of representable Nakayama--Hom duality in the module variable.

theorem MagnitudeConjecture.CoveringHom.representableNakayamaHomEquiv_projectiveNaturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : LinearModuleCategory k) {X Z : C} (q : X ⟶ Z) (a : M ⟶ dualLinearYonedaLinearModule Z) (f : linearCoyonedaLinearModule X ⟶ M) : ((representableNakayamaHomEquiv M X) (CategoryTheory.CategoryStruct.comp a (dualLinearYonedaLinearModuleMap q))) f = ((representableNakayamaHomEquiv M Z) a) (CategoryTheory.CategoryStruct.comp (linearCoyonedaLinearModuleMap q) f)

Naturality of representable Nakayama--Hom duality in the representing object.

noncomputable def MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaHomEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (X : C) (hP : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (M ⟶ finiteDimensionalDualLinearYoneda X hI) ≃ₗ[k] Module.Dual k (finiteDimensionalLinearCoyoneda X hP ⟶ M)

The same comparison inside the literal finite-dimensional module subcategory.

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaHomEquiv_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M N : FiniteDimensionalModuleCategory k} (X : C) (hP : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (g : M ⟶ N) (a : N ⟶ finiteDimensionalDualLinearYoneda X hI) (f : finiteDimensionalLinearCoyoneda X hP ⟶ M) : ((finiteRepresentableNakayamaHomEquiv M X hP hI) (CategoryTheory.CategoryStruct.comp g a)) f = ((finiteRepresentableNakayamaHomEquiv N X hP hI) a) (CategoryTheory.CategoryStruct.comp f g)

Naturality of the finite-dimensional representable comparison in the module variable.

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaHomEquiv_projectiveNaturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) {X Z : C} (q : X ⟶ Z) (hPX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hPZ : IsFiniteDimensionalModule k (linearCoyonedaLinearModule Z)) (hIX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hIZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) (a : M ⟶ finiteDimensionalDualLinearYoneda Z hIZ) (f : finiteDimensionalLinearCoyoneda X hPX ⟶ M) : ((finiteRepresentableNakayamaHomEquiv M X hPX hIX) (CategoryTheory.CategoryStruct.comp a (finiteDimensionalDualLinearYonedaMap q hIX hIZ))) f = ((finiteRepresentableNakayamaHomEquiv M Z hPZ hIZ) a) (CategoryTheory.CategoryStruct.comp (finiteDimensionalLinearCoyonedaMap q hPX hPZ) f)

Naturality of the finite-dimensional comparison in the representing object.

def MagnitudeConjecture.CoveringHom.finitePiDualToDualPi {k : Type v} [Field k] {ι : Type u_1} [Fintype ι] (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] : ((i : ι) → Module.Dual k (V i)) →ₗ[k] Module.Dual k ((i : ι) → V i)

Pair a finite family of coefficient functionals with a vector in the product by summing its component pairings.

noncomputable def MagnitudeConjecture.CoveringHom.dualPiToFinitePiDual {k : Type v} [Field k] {ι : Type u_1} [Fintype ι] (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] : Module.Dual k ((i : ι) → V i) →ₗ[k] (i : ι) → Module.Dual k (V i)

Restrict a functional on a finite product to each coordinate.

noncomputable def MagnitudeConjecture.CoveringHom.finitePiDualEquivDualPi {k : Type v} [Field k] {ι : Type u_1} [Fintype ι] (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] : ((i : ι) → Module.Dual k (V i)) ≃ₗ[k] Module.Dual k ((i : ι) → V i)

For a finite family, a family of coefficient functionals is canonically a functional on the product.

@[simp]

theorem MagnitudeConjecture.CoveringHom.finitePiDualEquivDualPi_apply {k : Type v} [Field k] {ι : Type u_1} [Fintype ι] (V : ι → Type w) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] (Phi : (i : ι) → Module.Dual k (V i)) (x : (i : ι) → V i) : ((finitePiDualEquivDualPi V) Phi) x = ∑ i : ι, (Phi i) (x i)

noncomputable def MagnitudeConjecture.CoveringHom.finiteRepresentableSumNakayamaHomEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (Q : CategoryTheory.Mat_ Cᵒᵖ) (M : FiniteDimensionalModuleCategory k) : (M ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q) ≃ₗ[k] Module.Dual k ((finiteProjectiveRepresentableSumFunctor hP).obj Q ⟶ M)

Nakayama--Hom duality for a literal finite sum of representables. Both the projective and Nakayama objects are exactly the values of the two matrix functors used by the orbit push-down comparison.

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableSumNakayamaHomEquiv_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (Q : CategoryTheory.Mat_ Cᵒᵖ) (M : FiniteDimensionalModuleCategory k) (a : M ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q) (f : (finiteProjectiveRepresentableSumFunctor hP).obj Q ⟶ M) : ((finiteRepresentableSumNakayamaHomEquiv hP hI Q M) a) f = ∑ i : Q.ι, ((finiteRepresentableNakayamaHomEquiv M (Opposite.unop (Q.X i)) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp a (CategoryTheory.Limits.biproduct.π (fun (j : Q.ι) => (finiteDimensionalDualLinearYonedaFunctor hI).obj (Q.X j)) i))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (j : Q.ι) => (finiteDimensionalLinearCoyonedaFunctor hP).obj (Q.X j)) i) f)

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableSumNakayamaHomEquiv_naturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (Q : CategoryTheory.Mat_ Cᵒᵖ) {M N : FiniteDimensionalModuleCategory k} (g : M ⟶ N) (a : N ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q) (f : (finiteProjectiveRepresentableSumFunctor hP).obj Q ⟶ M) : ((finiteRepresentableSumNakayamaHomEquiv hP hI Q M) (CategoryTheory.CategoryStruct.comp g a)) f = ((finiteRepresentableSumNakayamaHomEquiv hP hI Q N) a) (CategoryTheory.CategoryStruct.comp f g)

Naturality of finite-sum Nakayama--Hom duality in the module variable.

theorem MagnitudeConjecture.CoveringHom.finiteRepresentableSumNakayamaHomEquiv_projectiveNaturality {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {Q' Q : CategoryTheory.Mat_ Cᵒᵖ} (d : Q' ⟶ Q) (M : FiniteDimensionalModuleCategory k) (a : M ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q') (f : (finiteProjectiveRepresentableSumFunctor hP).obj Q ⟶ M) : ((finiteRepresentableSumNakayamaHomEquiv hP hI Q M) (CategoryTheory.CategoryStruct.comp a ((finiteNakayamaRepresentableSumFunctor hI).map d))) f = ((finiteRepresentableSumNakayamaHomEquiv hP hI Q' M) a) (CategoryTheory.CategoryStruct.comp ((finiteProjectiveRepresentableSumFunctor hP).map d) f)

Naturality of finite-sum Nakayama--Hom duality in the literal matrix of representing objects.