The representable resolution of a covariant defect

For a short exact sequence 0 → A → B → C → 0, the covariant representables form the exact sequence

0 → Hom(C,-) → Hom(B,-) → Hom(A,-) → G → 0.

This file splits that resolution into the two short exact sequences used to compute the reverse coherent dual of G.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.ShortComplex S.FiniteCovariantFunctor

The three covariant representables induced by a module short complex, in their contravariant order.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentableMap_mono_of_epi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : FG} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Mono (S.finiteRestrictedCovariantRepresentableMap f)

A covariant representable map induced by an epimorphism is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableComplex_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteCovariantRepresentableComplex K).Exact

Covariant Yoneda carries a short exact module sequence to an exact sequence at the middle representable.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectSyzygy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CoveringHom.FiniteDimensionalModuleCategory k

The first syzygy in the projective resolution of a covariant defect.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectSyzygyι {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : S.finiteCovariantDefectSyzygy K ⟶ S.finiteRestrictedCovariantRepresentable K.X₁

Exactness lets the second covariant-representable map descend through the first cokernel.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectSyzygyπ_comp_ι {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.finiteRestrictedCovariantRepresentableMap K.g)) (S.finiteCovariantDefectSyzygyι K) = S.finiteRestrictedCovariantRepresentableMap K.f

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectSyzygyπ_comp_ι_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h : S.finiteRestrictedCovariantRepresentable K.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.finiteRestrictedCovariantRepresentableMap K.g)) (CategoryTheory.CategoryStruct.comp (S.finiteCovariantDefectSyzygyι K) h) = CategoryTheory.CategoryStruct.comp (S.finiteRestrictedCovariantRepresentableMap K.f) h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectSyzygyι_mono {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : CategoryTheory.Mono (S.finiteCovariantDefectSyzygyι K)

For a short exact module sequence, the descended map from the first syzygy into the last covariant representable is monic.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectLeftShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.ShortComplex S.FiniteCovariantFunctor

The left half of the covariant representable resolution.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectLeftShortComplex_shortExact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteCovariantDefectLeftShortComplex K).ShortExact

The left half is short exact.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectRightShortComplex {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : CategoryTheory.ShortComplex FG) : CategoryTheory.ShortComplex S.FiniteCovariantFunctor

The right half of the covariant representable resolution.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectRightShortComplex_shortExact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : (S.finiteCovariantDefectRightShortComplex K).ShortExact

The right half is short exact.