Orbit push-down of dual corepresentable modules

This file develops the injective-representable half of Gabriel's Nakayama comparison. The coefficient dual of Hom(-, X) is a covariant module, and shifting its source reindexes the orbit Hom decomposition by negation.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYoneda {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Functor C (ModuleCat k)

The coefficient dual of the contravariant representable Hom(-, X), regarded as a covariant linear module.

instance MagnitudeConjecture.CoveringHom.dualLinearYoneda_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : (dualLinearYoneda X).Additive

instance MagnitudeConjecture.CoveringHom.dualLinearYoneda_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Functor.Linear k (dualLinearYoneda X)

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModule {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : LinearModuleCategory k

The dual corepresentable bundled as an additive linear module.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X X' : C} (f : X ⟶ X') : dualLinearYoneda X' ⟶ dualLinearYoneda X

A morphism of representing objects acts covariantly on coefficient-dual corepresentables.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModuleMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X X' : C} (f : X ⟶ X') : dualLinearYonedaLinearModule X' ⟶ dualLinearYonedaLinearModule X

Bundled linear-module form of the map induced by a morphism of representing objects.

@[simp]

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaMap_id {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : dualLinearYonedaMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (dualLinearYoneda X)

@[simp]

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaMap_comp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : dualLinearYonedaMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (dualLinearYonedaMap g) (dualLinearYonedaMap f)

def MagnitudeConjecture.CoveringHom.rightCompInvLinearEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X X' : C} (e : X ≅ X') : (Y ⟶ X') ≃ₗ[k] Y ⟶ X

Right composition with the inverse of an isomorphism, bundled as the linear equivalence in the direction used by coefficient duality.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaMapIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X X' : C} (e : X ≅ X') : dualLinearYoneda X ≅ dualLinearYoneda X'

Coefficient-dual corepresentables are naturally invariant under changing their representing object by an isomorphism.

@[simp]

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaMapIso_hom {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X X' : C} (e : X ≅ X') : (dualLinearYonedaMapIso e).hom = dualLinearYonedaMap e.inv

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYoneda {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : FiniteDimensionalModuleCategory k

A dual corepresentable known to be pointwise finite-dimensional with finite object support.

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X X' : C} (f : X ⟶ X') (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hX' : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X')) : finiteDimensionalDualLinearYoneda X' hX' ⟶ finiteDimensionalDualLinearYoneda X hX

Bundled finite-dimensional form of the map induced by a morphism of representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.shiftSourceHomLinearEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b a : A) (hba : -b = a) : ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X) ≃ₗ[k] ShiftHom Y X a

Moving a shift from the source of a Hom space to the target gives a linear equivalence, with the degree written explicitly for later dependent reindexing.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomLinearEquiv_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b : A) (g : (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) : (shiftSourceHomLinearEquiv Y X b (-b) ⋯) g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftEquiv C b).unit.app Y) ((CategoryTheory.shiftFunctor C (-b)).map g)

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomLinearEquiv_symm_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b : A) (q : ShiftHom Y X (-b)) : (shiftSourceHomLinearEquiv Y X b (-b) ⋯).symm q = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C b).map q) ((CategoryTheory.shiftEquiv C b).counit.app X)

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomLinearEquiv_apply_eq_shiftHomComp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b : A) (g : (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) : (shiftSourceHomLinearEquiv Y X b (-b) ⋯) g = shiftHomComp' ⋯ (CategoryTheory.shiftShiftNeg Y b).inv (shiftHomZero g)

The source-shift equivalence is composition in the orbit category with the canonical morphism from an object to its shift.

theorem MagnitudeConjecture.CoveringHom.neg_negEquiv_symm {A : Type w} [AddGroup A] (a : A) : -(Equiv.symm (Equiv.neg A)) a = a

noncomputable def MagnitudeConjecture.CoveringHom.shiftSourceHomDirectSumEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) : (DirectSum A fun (b : A) => (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) ≃ₗ[k] ShiftOrbitHom A Y X

The source-shifted Hom direct sum is the usual target-shifted orbit Hom direct sum. The reindexing is b ↦ -b.

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomDirectSumEquiv_inclusion_neg {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (a : A) (g : (CategoryTheory.shiftFunctor C ((Equiv.symm (Equiv.neg A)) a)).obj Y ⟶ X) : (shiftSourceHomDirectSumEquiv Y X) ((directSumInclusion (fun (b : A) => (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) ((Equiv.symm (Equiv.neg A)) a)) g) = (shiftOrbitLof Y X a) ((shiftSourceHomLinearEquiv Y X ((Equiv.symm (Equiv.neg A)) a) a ⋯) g)

On the summand indexed by -a, the source-shifted Hom equivalence is the homogeneous degree-a inclusion.

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomDirectSumEquiv_symm_shiftOrbitLof {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (a : A) (q : ShiftHom Y X a) : (shiftSourceHomDirectSumEquiv Y X).symm ((shiftOrbitLof Y X a) q) = (directSumInclusion (fun (b : A) => (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) ((Equiv.symm (Equiv.neg A)) a)) ((shiftSourceHomLinearEquiv Y X ((Equiv.symm (Equiv.neg A)) a) a ⋯).symm q)

Inverse formula on a homogeneous orbit morphism.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (Y X : C) : ShiftOrbitHom A Y X →ₗ[k] Y ⟶ X

Projection of an orbit Hom to its ordinary degree-zero component.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap_shiftOrbitLof_zero {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (Y X : C) (g : ShiftHom Y X 0) : (shiftOrbitZeroComponentLinearMap Y X) ((shiftOrbitLof Y X 0) g) = (shiftHomZeroLinearEquiv Y X).symm g

theorem MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap_shiftOrbitLof_ne {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (Y X : C) {a : A} (ha : a ≠ 0) (g : ShiftHom Y X a) : (shiftOrbitZeroComponentLinearMap Y X) ((shiftOrbitLof Y X a) g) = 0

theorem MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap_comp_identityComponent {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] {Y Z : C} (X : C) (f : Y ⟶ Z) (q : ShiftOrbitHom A Z X) : (shiftOrbitZeroComponentLinearMap Y X) ((shiftOrbitCompHom ((shiftOrbitLof Y Z 0) (shiftHomZero f))) q) = CategoryTheory.CategoryStruct.comp f ((shiftOrbitZeroComponentLinearMap Z X) q)

Degree-zero projection intertwines left composition by an ordinary upstairs morphism with left composition in the orbit category.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap_identityComponent_comp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (Y : C) {X Z : C} (q : ShiftOrbitHom A Y X) (f : X ⟶ Z) : (shiftOrbitZeroComponentLinearMap Y Z) ((shiftOrbitCompHom q) ((shiftOrbitLof X Z 0) (shiftHomZero f))) = CategoryTheory.CategoryStruct.comp ((shiftOrbitZeroComponentLinearMap Y X) q) f

Degree-zero projection intertwines right composition by an ordinary upstairs morphism with right composition in the orbit category.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitZeroComponentLinearMap_fromShift_comp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b a : A) (hba : -b = a) (q : ShiftHom Y X a) : (shiftOrbitZeroComponentLinearMap ((CategoryTheory.shiftFunctor C b).obj Y) X) ((shiftOrbitCompHom (shiftOrbitFromShift Y b)) ((shiftOrbitLof Y X a) q)) = (shiftSourceHomLinearEquiv Y X b a hba).symm q

Precomposing a homogeneous orbit morphism of degree a = -b by the canonical morphism from the b-shift recovers the inverse source-shift adjunction in degree zero.

theorem MagnitudeConjecture.CoveringHom.shiftSourceHomDirectSumEquiv_symm_apply_component {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (Y X : C) (b : A) (q : ShiftOrbitHom A Y X) : (DirectSum.component k A (fun (c : A) => (CategoryTheory.shiftFunctor C c).obj Y ⟶ X) b) ((shiftSourceHomDirectSumEquiv Y X).symm q) = (shiftOrbitZeroComponentLinearMap ((CategoryTheory.shiftFunctor C b).obj Y) X) ((shiftOrbitCompHom (shiftOrbitFromShift Y b)) q)

The b-component of the inverse source-shift decomposition is obtained by precomposing downstairs with the canonical morphism from the b-shift and then taking degree zero.

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaOrbitPullupApp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X Y : C) : Module.Dual k (Y ⟶ X) →ₗ[k] Module.Dual k (ShiftOrbitHom A Y X)

A functional on ordinary Hom(Y, X) extends to orbit Hom by reading its degree-zero component.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaOrbitPullupApp_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) {Y Z : C} (f : Y ⟶ Z) (phi : Module.Dual k (Y ⟶ X)) : (dualLinearYonedaOrbitPullupApp X Z) ((CategoryTheory.ConcreteCategory.hom ((dualLinearYoneda X).map f)) phi) = (CategoryTheory.ConcreteCategory.hom ((dualLinearYoneda (have this := X; this)).map (ShiftOrbitCategory.identityComponentFunctor.map f))) ((dualLinearYonedaOrbitPullupApp X Y) phi)

The degree-zero extension is natural for ordinary upstairs morphisms. The statement is pointwise because its source and target module categories live in the Hom universes of C and of the orbit category, respectively.

theorem MagnitudeConjecture.CoveringHom.dualLinearYonedaOrbitPullupApp_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Z : C} (f : X ⟶ Z) (Y : C) (phi : Module.Dual k (Y ⟶ Z)) : (dualLinearYonedaOrbitPullupApp X Y) ((CategoryTheory.ConcreteCategory.hom ((dualLinearYonedaMap f).app Y)) phi) = (CategoryTheory.ConcreteCategory.hom ((dualLinearYonedaMap (ShiftOrbitCategory.identityComponentFunctor.map f)).app (have this := Y; this))) ((dualLinearYonedaOrbitPullupApp Z Y) phi)

The degree-zero extension is natural in the representing object.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparisonApp {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X Y : C) : orbitPushdownValue (dualLinearYoneda X) Y →ₗ[k] Module.Dual k (ShiftOrbitHom A Y X)

The adjointly assembled comparison from push-down of a dual corepresentable to the downstairs dual corepresentable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparisonApp_lof {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X Y : C) (b : A) (phi : Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X)) : (orbitPushdownDualLinearYonedaComparisonApp X Y) ((orbitPushdownLof (dualLinearYoneda X) Y b) phi) = (CategoryTheory.ConcreteCategory.hom ((dualLinearYoneda (have this := X; this)).map (shiftOrbitFromShift Y b))) ((dualLinearYonedaOrbitPullupApp X ((CategoryTheory.shiftFunctor C b).obj Y)) phi)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparisonApp_naturality_homogeneous {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) {Y Z : C} (a : A) (f : ShiftHom Y Z a) : orbitPushdownDualLinearYonedaComparisonApp X Z ∘ₗ orbitPushdownHomogeneousMap (dualLinearYoneda X) a f = ModuleCat.Hom.hom ((dualLinearYoneda (have this := X; this)).map ((shiftOrbitOf Y Z a) f)) ∘ₗ orbitPushdownDualLinearYonedaComparisonApp X Y

The assembled comparison is natural for a homogeneous orbit morphism.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparisonApp_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) {Y Z : C} (f : ShiftOrbitHom A Y Z) : orbitPushdownDualLinearYonedaComparisonApp X Z ∘ₗ (orbitPushdownMapLinear (dualLinearYoneda X)) f = ModuleCat.Hom.hom ((dualLinearYoneda (have this := X; this)).map f) ∘ₗ orbitPushdownDualLinearYonedaComparisonApp X Y

The assembled comparison is natural for every orbit morphism.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparison {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) : orbitPushdown (dualLinearYoneda X) ⟶ dualLinearYoneda (have this := X; this)

Orbit push-down of a dual corepresentable maps naturally to the downstairs dual corepresentable.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparison_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Z : C} (f : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans (dualLinearYonedaMap f)) (orbitPushdownDualLinearYonedaComparison X) = CategoryTheory.CategoryStruct.comp (orbitPushdownDualLinearYonedaComparison Z) (dualLinearYonedaMap (ShiftOrbitCategory.identityComponentFunctor.map f))

The push-down comparison commutes with morphisms of representing objects. This is the square needed to transport a projective-presentation differential through the Nakayama construction.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaValueEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X Y : C) (hY : {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) : orbitPushdownValue (dualLinearYoneda X) Y ≃ₗ[k] Module.Dual k (ShiftOrbitHom A Y X)

The objectwise finite-duality comparison underlying push-down of a dual corepresentable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaValueEquiv_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X Y : C) (hY : {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) (Phi : orbitPushdownValue (dualLinearYoneda X) Y) (q : ShiftOrbitHom A Y X) : ((orbitPushdownDualLinearYonedaValueEquiv X Y hY) Phi) q = ((directSumDualToDual fun (b : A) => (CategoryTheory.shiftFunctor C b).obj Y ⟶ X) Phi) ((shiftSourceHomDirectSumEquiv Y X).symm q)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaComparisonApp_eq_valueEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X Y : C) (hY : {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) : orbitPushdownDualLinearYonedaComparisonApp X Y = ↑(orbitPushdownDualLinearYonedaValueEquiv X Y hY)

Under finite support, the naturally assembled comparison is exactly the basis-free direct-sum duality equivalence.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) (hX : ∀ (Y : C), {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) : orbitPushdown (dualLinearYoneda X) ≅ dualLinearYoneda (have this := X; this)

If the translated dual Hom values have finite support at every object, orbit push-down of a dual corepresentable is naturally isomorphic to the downstairs dual corepresentable.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaIso_hom_eq_comparison {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (X : C) (hX : ∀ (Y : C), {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) : (orbitPushdownDualLinearYonedaIso X hX).hom = orbitPushdownDualLinearYonedaComparison X

The forward map of the finite dual-corepresentable isomorphism is the unrestricted natural comparison constructed above.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] {X Z : C} (f : X ⟶ Z) (hX : ∀ (Y : C), {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ X))}.Finite) (hZ : ∀ (Y : C), {b : A | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor C b).obj Y ⟶ Z))}.Finite) : CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans (dualLinearYonedaMap f)) (orbitPushdownDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (orbitPushdownDualLinearYonedaIso Z hZ).hom (dualLinearYonedaMap (ShiftOrbitCategory.identityComponentFunctor.map f))

The finite push-down isomorphisms commute with morphisms of representing objects.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.dualLinearYonedaMap_objectIsoDeckOrbitRepresentative_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (dualLinearYonedaMap (ShiftOrbitCategory.identityComponentFunctor.map f)) (dualLinearYonedaMapIso (D.objectIsoDeckOrbitRepresentative X)).hom = CategoryTheory.CategoryStruct.comp (dualLinearYonedaMapIso (D.objectIsoDeckOrbitRepresentative Z)).hom (dualLinearYonedaMap (deckOrbitRepresentativeFunctor.map (D.orbitSkeletonMap f)))

Changing an upstairs representing object and then moving it to the chosen orbit representative agrees with first moving both objects and then applying the induced skeletal morphism.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (q : MulAction.orbitRel.Quotient G C) : deckOrbitRepresentativeFunctor.comp (dualLinearYoneda (have this := deckOrbitRepresentative q; this)) ≅ dualLinearYoneda q

Restricting the orbit dual corepresentable at a chosen representative gives the literal dual corepresentable on the induced orbit skeleton.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.deckOrbitRepresentativeDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {q r : MulAction.orbitRel.Quotient G C} (f : (have this := q; this) ⟶ have this := r; this) : CategoryTheory.CategoryStruct.comp (deckOrbitRepresentativeFunctor.whiskerLeft (dualLinearYonedaMap (deckOrbitRepresentativeFunctor.map f))) (D.deckOrbitRepresentativeDualLinearYonedaIso q).hom = CategoryTheory.CategoryStruct.comp (D.deckOrbitRepresentativeDualLinearYonedaIso r).hom (dualLinearYonedaMap f)

Restriction from the shift-orbit category to the chosen orbit skeleton commutes with morphisms of representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownDualLinearYonedaValueEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (Y : C) : orbitPushdownValue (dualLinearYoneda X) Y ≃ₗ[k] Module.Dual k (ShiftOrbitHom (Additive G) Y X)

For a finite dual corepresentable, the objectwise comparison is available at every upstairs object from literal finite support and freeness of the deck action.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : orbitPushdown (dualLinearYoneda X) ≅ dualLinearYoneda (have this := X; this)

Deck freeness and finite support make the objectwise comparison a natural isomorphism on the full shift-orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitPushdownDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) : CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans (dualLinearYonedaMap f)) (D.orbitPushdownDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (D.orbitPushdownDualLinearYonedaIso Z hZ).hom (dualLinearYonedaMap (ShiftOrbitCategory.identityComponentFunctor.map f))

The deck-finite orbit-category comparison commutes with morphisms of representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : orbitSkeletonPushdown (dualLinearYoneda X) ≅ dualLinearYoneda (Quotient.mk'' X)

Skeletal Gabriel push-down sends a finite dual corepresentable to the dual corepresentable at the strict orbit of its representing object.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdownDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) : CategoryTheory.CategoryStruct.comp (deckOrbitRepresentativeFunctor.whiskerLeft (orbitPushdownNatTrans (dualLinearYonedaMap f))) (D.orbitSkeletonPushdownDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (D.orbitSkeletonPushdownDualLinearYonedaIso Z hZ).hom (dualLinearYonedaMap (D.orbitSkeletonMap f))

The skeletal dual-corepresentable isomorphisms commute with the morphism between strict deck orbits induced by an upstairs representing morphism.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : linearModuleOrbitSkeletonPushdown.obj (dualLinearYonedaLinearModule X) ≅ dualLinearYonedaLinearModule (Quotient.mk'' X)

Bundled linear-module form of skeletal push-down preserving a finite dual corepresentable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso_hom_hom {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (D.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso X hX).hom.hom = (D.orbitSkeletonPushdownDualLinearYonedaIso X hX).hom

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) : CategoryTheory.CategoryStruct.comp (linearModuleOrbitSkeletonPushdown.map (dualLinearYonedaLinearModuleMap f)) (D.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (D.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso Z hZ).hom (dualLinearYonedaLinearModuleMap (D.orbitSkeletonMap f))

The skeletal comparison is natural in the representing object inside the literal category of additive linear modules.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalDualLinearYoneda {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : FiniteDimensionalModuleCategory k

The downstairs skeletal dual corepresentable, with finiteness transported from its finite upstairs source through skeletal push-down.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalDualLinearYonedaMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) : D.orbitSkeletonFiniteDimensionalDualLinearYoneda Z hZ ⟶ D.orbitSkeletonFiniteDimensionalDualLinearYoneda X hX

The finite-dimensional skeletal dual corepresentables inherit the map induced by a morphism of upstairs representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj (finiteDimensionalDualLinearYoneda X hX) ≅ D.orbitSkeletonFiniteDimensionalDualLinearYoneda X hX

Literal finite-dimensional skeletal push-down preserves a finite dual corepresentable.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso_hom_hom {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (X : C) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (D.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso X hX).hom.hom = (D.linearModuleOrbitSkeletonPushdownDualLinearYonedaIso X hX).hom

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso_representing_naturality {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {X Z : C} (f : X ⟶ Z) (hX : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hZ : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule Z)) : CategoryTheory.CategoryStruct.comp (D.finiteDimensionalModuleOrbitSkeletonPushdown.map (finiteDimensionalDualLinearYonedaMap f hX hZ)) (D.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (D.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaIso Z hZ).hom (D.orbitSkeletonFiniteDimensionalDualLinearYonedaMap f hX hZ)

The literal finite-dimensional skeletal push-down comparison commutes with maps of representing objects.