Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteRepresentableNakayamaFull

Full faithfulness of finite-representable Nakayama duality #

The Nakayama images of literal finite sums of representables have the same Hom spaces as the projective sums themselves. The equivalence is obtained by applying the finite Nakayama--Hom pairing twice and using finite-dimensional double-dual evaluation. Its compatibility with composition is the exact interface needed by the minimal-presentation argument.

source
noncomputable def MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapLinearEquiv {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ᵒᵖ) :
((finiteProjectiveRepresentableSumFunctor hP).obj Q' ⟶ (finiteProjectiveRepresentableSumFunctor hP).obj Q) ≃ₗ[k] (finiteNakayamaRepresentableSumFunctor hI).obj Q' ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q

Nakayama duality is fully faithful on literal finite sums of representables.

Instances For
    source
    theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapLinearEquiv_pairing {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ᵒᵖ) (e : (finiteProjectiveRepresentableSumFunctor hP).obj Q' ⟶ (finiteProjectiveRepresentableSumFunctor hP).obj Q) (b : (finiteProjectiveRepresentableSumFunctor hP).obj Q ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q') :
    ((finiteRepresentableSumNakayamaHomEquiv hP hI Q ((finiteNakayamaRepresentableSumFunctor hI).obj Q')) ((finiteRepresentableNakayamaMapLinearEquiv hP hI Q' Q) e)) b = ((finiteRepresentableSumNakayamaHomEquiv hP hI Q' ((finiteProjectiveRepresentableSumFunctor hP).obj Q)) b) e

    The defining pairing identity for the finite-projective Nakayama map.

    source
    theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapLinearEquiv_map {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) :
    (finiteRepresentableNakayamaMapLinearEquiv hP hI Q' Q) ((finiteProjectiveRepresentableSumFunctor hP).map d) = (finiteNakayamaRepresentableSumFunctor hI).map d

    The equivalence sends a literal representing-object matrix to the map of that matrix under the finite Nakayama functor.

    source
    theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapLinearEquiv_comp {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₁ Q₂ : CategoryTheory.Mat_ Cᵒᵖ) (e : (finiteProjectiveRepresentableSumFunctor hP).obj Q₀ ⟶ (finiteProjectiveRepresentableSumFunctor hP).obj Q₁) (f : (finiteProjectiveRepresentableSumFunctor hP).obj Q₁ ⟶ (finiteProjectiveRepresentableSumFunctor hP).obj Q₂) :
    (finiteRepresentableNakayamaMapLinearEquiv hP hI Q₀ Q₂) (CategoryTheory.CategoryStruct.comp e f) = CategoryTheory.CategoryStruct.comp ((finiteRepresentableNakayamaMapLinearEquiv hP hI Q₀ Q₁) e) ((finiteRepresentableNakayamaMapLinearEquiv hP hI Q₁ Q₂) f)

    Nakayama maps of finite projective sums preserve composition.

    source
    @[simp]
    theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapLinearEquiv_id {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ᵒᵖ) :
    (finiteRepresentableNakayamaMapLinearEquiv hP hI Q Q) (CategoryTheory.CategoryStruct.id ((finiteProjectiveRepresentableSumFunctor hP).obj Q)) = CategoryTheory.CategoryStruct.id ((finiteNakayamaRepresentableSumFunctor hI).obj Q)
    source
    noncomputable def MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMapPreimage {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ᵒᵖ) (a : (finiteNakayamaRepresentableSumFunctor hI).obj Q' ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q) :
    (finiteProjectiveRepresentableSumFunctor hP).obj Q' ⟶ (finiteProjectiveRepresentableSumFunctor hP).obj Q

    The projective map corresponding to a morphism between finite Nakayama sums.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.finiteRepresentableNakayamaMap_preimage {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ᵒᵖ) (a : (finiteNakayamaRepresentableSumFunctor hI).obj Q' ⟶ (finiteNakayamaRepresentableSumFunctor hI).obj Q) :
      (finiteRepresentableNakayamaMapLinearEquiv hP hI Q' Q) (finiteRepresentableNakayamaMapPreimage hP hI Q' Q a) = a