Perfect composition pairings through fully faithful functors

A natural isomorphism from a covariant representable to a coefficient-dual corepresentable is equivalent to a perfect composition pairing. This file records the part of that construction which is preserved by a fully faithful linear functor. It is used to pass a Nakayama pairing from a deck-orbit category to its full image in a mesh category.

noncomputable def MagnitudeConjecture.CoveringHom.fullyFaithfulMapLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (X Y : C) : (X ⟶ Y) ≃ₗ[k] F.obj X ⟶ F.obj Y

A fully faithful linear functor identifies every source Hom space with the corresponding Hom space between its images.

@[simp]

theorem MagnitudeConjecture.CoveringHom.fullyFaithfulMapLinearEquiv_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) : (fullyFaithfulMapLinearEquiv F X Y) f = F.map f

noncomputable def MagnitudeConjecture.CoveringHom.linearModuleIsoEpsilon {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (P J : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) : (P ⟶ J) →ₗ[k] k

Evaluation at the target identity extracts the composition functional from a representable/dual-corepresentable natural isomorphism.

theorem MagnitudeConjecture.CoveringHom.linearModuleIsoEpsilon_comp {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (P J X : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) (f : P ⟶ X) (g : X ⟶ J) : (linearModuleIsoEpsilon P J e) (CategoryTheory.CategoryStruct.comp f g) = (have this := (CategoryTheory.ConcreteCategory.hom (e.hom.hom.app X)) f; this) g

Naturality identifies every component of the module isomorphism with composition followed by its extracted functional.

noncomputable def MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoEpsilon {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) : (F.obj P ⟶ F.obj J) →ₗ[k] k

The composition functional transported to the image of a fully faithful linear functor.

theorem MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoEpsilon_map_comp_map {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J X : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) (f : P ⟶ X) (g : X ⟶ J) : (fullyFaithfulLinearModuleIsoEpsilon F P J e) (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) = (have this := (CategoryTheory.ConcreteCategory.hom (e.hom.hom.app X)) f; this) g

On mapped morphisms, the transported functional recovers the component of the original natural isomorphism.

noncomputable def MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoPairingEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J X : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) : (F.obj P ⟶ F.obj X) ≃ₗ[k] Module.Dual k (F.obj X ⟶ F.obj J)

The perfect pairing induced at an object in the image of a fully faithful linear functor.

theorem MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoPairingEquiv_apply_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J X : C) (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) (q : F.obj P ⟶ F.obj X) (r : F.obj X ⟶ F.obj J) : ((fullyFaithfulLinearModuleIsoPairingEquiv F P J X e) q) r = (fullyFaithfulLinearModuleIsoEpsilon F P J e) (CategoryTheory.CategoryStruct.comp q r)

The transported pairing equivalence is literally composition followed by the transported functional.

noncomputable def MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoEpsilonCongr {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J : C) (P' J' : D) (iP : F.obj P ≅ P') (iJ : F.obj J ≅ J') (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) : (P' ⟶ J') →ₗ[k] k

The transported composition functional after replacing its two endpoint objects by isomorphic objects in the target category.

noncomputable def MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoPairingEquivCongr {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J X : C) (P' J' X' : D) (iP : F.obj P ≅ P') (iJ : F.obj J ≅ J') (iX : F.obj X ≅ X') (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) : (P' ⟶ X') ≃ₗ[k] Module.Dual k (X' ⟶ J')

The perfect pairing transported through a fully faithful functor and through chosen isomorphisms of all three endpoint objects.

theorem MagnitudeConjecture.CoveringHom.fullyFaithfulLinearModuleIsoPairingEquivCongr_apply_apply {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [F.Faithful] (P J X : C) (P' J' X' : D) (iP : F.obj P ≅ P') (iJ : F.obj J ≅ J') (iX : F.obj X ≅ X') (e : linearCoyonedaLinearModule P ≅ dualLinearYonedaLinearModule J) (q : P' ⟶ X') (r : X' ⟶ J') : ((fullyFaithfulLinearModuleIsoPairingEquivCongr F P J X P' J' X' iP iJ iX e) q) r = (fullyFaithfulLinearModuleIsoEpsilonCongr F P J P' J' iP iJ e) (CategoryTheory.CategoryStruct.comp q r)

After all object transports, the perfect pairing remains evaluation of one functional on composition.