The finite-projective Nakayama--Hom pairing for right modules

This file develops the concrete comparison

Hom_B(Y, D Hom_B(P,B)) \simeq D Hom_B(P,Y)

for a finitely generated projective right module P. It is the duality input for identifying the Nakayama kernel of a minimal presentation with the Auslander--Reiten translate. The proof uses only the finite frame already constructed in RightModuleNakayama.

noncomputable def MagnitudeConjecture.RightModule.projectiveFrame {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : FiniteProjectiveFrame Bᵐᵒᵖ ↑P

A chosen finite dual frame on a finitely generated projective right module.

noncomputable def MagnitudeConjecture.RightModule.projectiveFrameRegularHom {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (i : Fin (projectiveFrame P).n) : regularHomDualCarrier P

The regular-Hom functional associated with one member of a projective frame.

def MagnitudeConjecture.RightModule.projectiveRankOne {B : Type u} [Ring B] (P Y : FGModuleCat Bᵐᵒᵖ) (q : regularHomDualCarrier P) (y : ↑Y) : ↑P →ₗ[Bᵐᵒᵖ] ↑Y

The rank-one right-module map determined by a regular-Hom functional and an element of the target.

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveRankOne_add_left {B : Type u} [Ring B] (P Y : FGModuleCat Bᵐᵒᵖ) (q q' : regularHomDualCarrier P) (y : ↑Y) : projectiveRankOne P Y (q + q') y = projectiveRankOne P Y q y + projectiveRankOne P Y q' y

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveRankOne_add_right {B : Type u} [Ring B] (P Y : FGModuleCat Bᵐᵒᵖ) (q : regularHomDualCarrier P) (y y' : ↑Y) : projectiveRankOne P Y q (y + y') = projectiveRankOne P Y q y + projectiveRankOne P Y q y'

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveRankOne_balance {B : Type u} [Ring B] (P Y : FGModuleCat Bᵐᵒᵖ) (b : B) (q : regularHomDualCarrier P) (y : ↑Y) : projectiveRankOne P Y q (MulOpposite.op b • y) = projectiveRankOne P Y (b • q) y

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveRankOne_smul_left {k B : Type u} [Field k] [Ring B] [Algebra k B] (P Y : FGModuleCat Bᵐᵒᵖ) (a : k) (q : regularHomDualCarrier P) (y : ↑Y) : projectiveRankOne P Y (a • q) y = a • projectiveRankOne P Y q y

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveRankOne_smul_right {k B : Type u} [Field k] [Ring B] [Algebra k B] (P Y : FGModuleCat Bᵐᵒᵖ) (a : k) (q : regularHomDualCarrier P) (y : ↑Y) : projectiveRankOne P Y q (a • y) = a • projectiveRankOne P Y q y

def MagnitudeConjecture.RightModule.nakayamaHomValue {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) (ell : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y)) (y : ↑Y) : ↑(projectiveNakayamaFGObj P)

Evaluation of a dual Hom functional against the rank-one pairing.

def MagnitudeConjecture.RightModule.nakayamaHomRLinear {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) (ell : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y)) : ↑Y →ₗ[Bᵐᵒᵖ] ↑(projectiveNakayamaFGObj P)

The Nakayama--Hom pairing as a right-module map in the variable module.

def MagnitudeConjecture.RightModule.nakayamaHomLinearMap {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y) →ₗ[k] ↑Y →ₗ[Bᵐᵒᵖ] ↑(projectiveNakayamaFGObj P)

The Nakayama--Hom pairing as a k-linear map.

theorem MagnitudeConjecture.RightModule.projectiveRankOne_frame_sum {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (f : ↑P →ₗ[Bᵐᵒᵖ] ↑Y) : ∑ i : Fin (projectiveFrame P).n, projectiveRankOne P Y (projectiveFrameRegularHom P i) (f ((projectiveFrame P).p i)) = f

The chosen projective frame expands every morphism as a finite sum of rank-one maps.

theorem MagnitudeConjecture.RightModule.regularHomDual_frame_sum {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (q : regularHomDualCarrier P) : ∑ i : Fin (projectiveFrame P).n, q ((projectiveFrame P).p i) • projectiveFrameRegularHom P i = q

The same frame reconstructs every element of the regular Hom-dual.

noncomputable def MagnitudeConjecture.RightModule.regularHomDualMapPreimage {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Q : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective Q] (h : regularHomDualFGObj k Q ⟶ regularHomDualFGObj k P) : P ⟶ Q

Recover a map of finite projective right modules from the induced map between their regular Hom-duals.

theorem MagnitudeConjecture.RightModule.regularHomDualMap_preimage {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Q : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective Q] (h : regularHomDualFGObj k Q ⟶ regularHomDualFGObj k P) : regularHomDualMap (regularHomDualMapPreimage P Q h) = h

Regular-Hom dualization is full on finite projective right modules.

noncomputable def MagnitudeConjecture.RightModule.projectiveNakayamaMapPreimage {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Q : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective Q] (a : projectiveNakayamaFGObj P ⟶ projectiveNakayamaFGObj Q) : P ⟶ Q

Recover a map of finite projective right modules from a morphism between their Nakayama objects.

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_preimage {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Q : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective Q] (a : projectiveNakayamaFGObj P ⟶ projectiveNakayamaFGObj Q) : projectiveNakayamaMap (projectiveNakayamaMapPreimage P Q a) = a

The concrete Nakayama construction is full on finite projectives.

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Q : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective Q] : Function.Injective fun (d : P ⟶ Q) => projectiveNakayamaMap d

The concrete Nakayama construction is faithful on finite projectives.

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_comp {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q T : FGModuleCat Bᵐᵒᵖ} (d : P ⟶ Q) (e : Q ⟶ T) : projectiveNakayamaMap (CategoryTheory.CategoryStruct.comp d e) = CategoryTheory.CategoryStruct.comp (projectiveNakayamaMap d) (projectiveNakayamaMap e)

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_id {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) : projectiveNakayamaMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (projectiveNakayamaFGObj P)

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_add {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d e : P ⟶ Q) : projectiveNakayamaMap (d + e) = projectiveNakayamaMap d + projectiveNakayamaMap e

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_smul {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (c : k) (d : P ⟶ Q) : projectiveNakayamaMap (c • d) = c • projectiveNakayamaMap d

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_sub {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P Q : FGModuleCat Bᵐᵒᵖ} (d e : P ⟶ Q) : projectiveNakayamaMap (d - e) = projectiveNakayamaMap d - projectiveNakayamaMap e

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaMap_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Q : FGModuleCat Bᵐᵒᵖ) : projectiveNakayamaMap 0 = 0

noncomputable def MagnitudeConjecture.RightModule.projectiveNakayamaEndRingEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : CategoryTheory.End P ≃+* CategoryTheory.End (projectiveNakayamaFGObj P)

On a finite projective right module, the concrete Nakayama functor induces an equivalence of endomorphism rings.

noncomputable def MagnitudeConjecture.RightModule.regularHomDualFreeSection {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : regularHomDualCarrier P →ₗ[B] Fin (projectiveFrame P).n → B

Coordinates of the regular Hom-dual in the frame inherited from P.

noncomputable def MagnitudeConjecture.RightModule.regularHomDualFreeRetraction {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : (Fin (projectiveFrame P).n → B) →ₗ[B] regularHomDualCarrier P

Reconstruction from the inherited regular-Hom frame.

theorem MagnitudeConjecture.RightModule.regularHomDual_moduleProjective {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : Module.Projective B (regularHomDualCarrier P)

The regular Hom-dual of a finite projective right module is a finite projective left module.

theorem MagnitudeConjecture.RightModule.projectiveNakayamaFGObj_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : CategoryTheory.Injective (projectiveNakayamaFGObj P)

The concrete Nakayama object of a finite projective right module is injective.

theorem MagnitudeConjecture.RightModule.nakayamaHomLinearMap_injective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : Function.Injective ⇑(nakayamaHomLinearMap P Y)

The Nakayama--Hom pairing is injective for a projective source.

def MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (z : ↑(projectiveNakayamaFGObj P)) (q : ↑(regularHomDualFGObj k P)) : k

Evaluation of an element of nu P on the regular-Hom dual.

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_add {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (z z' : ↑(projectiveNakayamaFGObj P)) (q : ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P (z + z') q = projectiveNakayamaEvaluation P z q + projectiveNakayamaEvaluation P z' q

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_smul {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (b : Bᵐᵒᵖ) (z : ↑(projectiveNakayamaFGObj P)) (q : ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P (b • z) q = projectiveNakayamaEvaluation P z (MulOpposite.unop b • q)

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_ksmul {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) (a : k) (z : ↑(projectiveNakayamaFGObj P)) (q : ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P (a • z) q = a * projectiveNakayamaEvaluation P z q

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_sum {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P : FGModuleCat Bᵐᵒᵖ) {n : ℕ} (z : ↑(projectiveNakayamaFGObj P)) (v : Fin n → ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P z (∑ i : Fin n, v i) = ∑ i : Fin n, projectiveNakayamaEvaluation P z (v i)

@[simp]

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_nakayamaHomValue {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (P Y : FGModuleCat Bᵐᵒᵖ) (ell : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y)) (y : ↑Y) (q : ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P (nakayamaHomValue P Y ell y) q = ell (projectiveRankOne P Y q y)

noncomputable def MagnitudeConjecture.RightModule.nakayamaHomInverseFunctional {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (g : ↑Y →ₗ[Bᵐᵒᵖ] ↑(projectiveNakayamaFGObj P)) : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y)

The explicit inverse functional furnished by the projective frame.

theorem MagnitudeConjecture.RightModule.nakayamaHomLinearMap_surjective {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : Function.Surjective ⇑(nakayamaHomLinearMap P Y)

The Nakayama--Hom pairing is surjective for a projective source.

noncomputable def MagnitudeConjecture.RightModule.nakayamaHomLinearEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : Module.Dual k (↑P →ₗ[Bᵐᵒᵖ] ↑Y) ≃ₗ[k] ↑Y →ₗ[Bᵐᵒᵖ] ↑(projectiveNakayamaFGObj P)

The concrete finite-projective Nakayama--Hom comparison.

def MagnitudeConjecture.RightModule.fgHomCarrierLinearEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] (Y Z : FGModuleCat Bᵐᵒᵖ) : (Y ⟶ Z) ≃ₗ[k] ↑Y →ₗ[Bᵐᵒᵖ] ↑Z

Categorical morphisms in FGModuleCat identified with their underlying right-module maps, including the restricted k-linear structure.

noncomputable def MagnitudeConjecture.RightModule.fieldNakayamaHomEquiv {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] : (Y ⟶ projectiveNakayamaFGObj P) ≃ₗ[k] (P ⟶ Y) →ₗ[k] k

The field-valued Nakayama--Hom equivalence in categorical form.

@[simp]

theorem MagnitudeConjecture.RightModule.fieldNakayamaHomEquiv_rankOne {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (a : Y ⟶ projectiveNakayamaFGObj P) (q : ↑(regularHomDualFGObj k P)) (y : ↑Y) : ((fieldNakayamaHomEquiv P Y) a) (FGModuleCat.ofHom (projectiveRankOne P Y q y)) = projectiveNakayamaEvaluation P ((ModuleCat.Hom.hom a.hom) y) q

theorem MagnitudeConjecture.RightModule.categoricalProjectiveRankOne_frame_sum {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (f : P ⟶ Y) : ∑ i : Fin (projectiveFrame P).n, FGModuleCat.ofHom (projectiveRankOne P Y (projectiveFrameRegularHom P i) ((ModuleCat.Hom.hom f.hom) ((projectiveFrame P).p i))) = f

The categorical finite rank-one expansion.

theorem MagnitudeConjecture.RightModule.fieldNakayamaHomEquiv_apply_eq_sum {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P Y : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] (a : Y ⟶ projectiveNakayamaFGObj P) (f : P ⟶ Y) : ((fieldNakayamaHomEquiv P Y) a) f = ∑ i : Fin (projectiveFrame P).n, projectiveNakayamaEvaluation P ((ModuleCat.Hom.hom a.hom) ((ModuleCat.Hom.hom f.hom) ((projectiveFrame P).p i))) (projectiveFrameRegularHom P i)

Every value of the categorical comparison is its finite-frame sum.

theorem MagnitudeConjecture.RightModule.fieldNakayamaHomEquiv_naturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (P : FGModuleCat Bᵐᵒᵖ) [CategoryTheory.Projective P] {Y Z : FGModuleCat Bᵐᵒᵖ} (g : Y ⟶ Z) (a : Z ⟶ projectiveNakayamaFGObj P) (f : P ⟶ Y) : ((fieldNakayamaHomEquiv P Y) (CategoryTheory.CategoryStruct.comp g a)) f = ((fieldNakayamaHomEquiv P Z) a) (CategoryTheory.CategoryStruct.comp f g)

Naturality of the field Nakayama--Hom comparison in the variable module.

theorem MagnitudeConjecture.RightModule.projectiveRankOne_projectiveNaturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P' P : FGModuleCat Bᵐᵒᵖ} (d : P' ⟶ P) (Y : FGModuleCat Bᵐᵒᵖ) (q : regularHomDualCarrier P) (y : ↑Y) : projectiveRankOne P Y q y ∘ₗ ModuleCat.Hom.hom d.hom = projectiveRankOne P' Y ((ModuleCat.Hom.hom (regularHomDualMap d).hom) q) y

Rank-one maps are natural in their projective source.

theorem MagnitudeConjecture.RightModule.projectiveNakayamaEvaluation_map {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] {P' P : FGModuleCat Bᵐᵒᵖ} (d : P' ⟶ P) (z : ↑(projectiveNakayamaFGObj P')) (q : ↑(regularHomDualFGObj k P)) : projectiveNakayamaEvaluation P ((ModuleCat.Hom.hom (projectiveNakayamaMap d).hom) z) q = projectiveNakayamaEvaluation P' z ((ModuleCat.Hom.hom (regularHomDualMap d).hom) q)

Evaluation is natural under the covariant Nakayama map.

theorem MagnitudeConjecture.RightModule.categoricalProjectiveRankOne_projective_frame_sum {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {P' P : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.Projective P] (d : P' ⟶ P) (Y : FGModuleCat Bᵐᵒᵖ) (f : P ⟶ Y) : ∑ i : Fin (projectiveFrame P).n, FGModuleCat.ofHom (projectiveRankOne P' Y ((ModuleCat.Hom.hom (regularHomDualMap d).hom) (projectiveFrameRegularHom P i)) ((ModuleCat.Hom.hom f.hom) ((projectiveFrame P).p i))) = CategoryTheory.CategoryStruct.comp d f

A projective-frame expansion remains valid after precomposition by a map of projectives.

theorem MagnitudeConjecture.RightModule.fieldNakayamaHomEquiv_projectiveNaturality {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {P' P : FGModuleCat Bᵐᵒᵖ} [CategoryTheory.Projective P'] [CategoryTheory.Projective P] (d : P' ⟶ P) (Y : FGModuleCat Bᵐᵒᵖ) (a : Y ⟶ projectiveNakayamaFGObj P') (f : P ⟶ Y) : ((fieldNakayamaHomEquiv P Y) (CategoryTheory.CategoryStruct.comp a (projectiveNakayamaMap d))) f = ((fieldNakayamaHomEquiv P' Y) a) (CategoryTheory.CategoryStruct.comp d f)

Naturality of the Nakayama--Hom comparison in the finite-projective variable.