Coherent duality on exact defects

This file packages the two pointwise Ext² calculations as functors on the full subcategories of defects admitting exact representable presentations.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (F : S.FiniteContravariantDefectCategory) : CategoryTheory.ShortComplex FG

A chosen exact presentation of a contravariant defect.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectPresentation_shortExact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (F : S.FiniteContravariantDefectCategory) : (S.contravariantDefectPresentation F).ShortExact

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contravariantDefectPresentationIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (F : S.FiniteContravariantDefectCategory) : S.finiteContravariantDefect (S.contravariantDefectPresentation F) ≅ F.obj

Identification of the defect of the chosen presentation with the given contravariant defect.

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

A chosen exact presentation of a covariant defect.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectPresentation_shortExact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantDefectCategory) : (S.covariantDefectPresentation G).ShortExact

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.covariantDefectPresentationIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (G : S.FiniteCovariantDefectCategory) : S.finiteCovariantDefect (S.covariantDefectPresentation G) ≅ G.obj

Identification of the defect of the chosen presentation with the given covariant defect.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenCovariantDefectCoherentDualIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (F : S.FiniteContravariantDefectCategory) : S.finiteCovariantFunctorInclusion.obj (S.finiteCovariantDefect (S.contravariantDefectPresentation F)) ≅ S.coherentDualObj F.obj

The coherent dual of a contravariant defect is identified with the covariant defect of its chosen exact presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenContravariantDefectCoherentCodualIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantDefectCategory) : S.finiteContravariantFunctorInclusion.obj (S.finiteContravariantDefect (S.covariantDefectPresentation G)) ≅ S.coherentCodualObj G.obj

The reverse coherent dual of a covariant defect is identified with the contravariant defect of its chosen exact presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteContravariantFunctor] : CategoryTheory.Functor S.FiniteContravariantDefectCategoryᵒᵖ (CategoryTheory.Functor S.IndecCategory (ModuleCat k))

The raw coherent dual restricted to exact contravariant defects.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsRaw_isLinear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (F : S.FiniteContravariantDefectCategoryᵒᵖ) : CoveringHom.IsLinearModule k (S.coherentDualOnContravariantDefectsRaw.obj F)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsLinear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteContravariantDefectCategoryᵒᵖ (CoveringHom.LinearModuleCategory k)

The coherent dual on exact contravariant defects, valued in linear modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsLinear_isFiniteDimensional {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (F : S.FiniteContravariantDefectCategoryᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (S.coherentDualOnContravariantDefectsLinear.obj F)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteContravariantDefectCategoryᵒᵖ S.FiniteCovariantFunctor

The coherent dual restricted to exact contravariant defects, valued in finite linear functors.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefectsFinite_isDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (F : S.FiniteContravariantDefectCategoryᵒᵖ) : S.IsFiniteCovariantDefect (S.coherentDualOnContravariantDefectsFinite.obj F)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefects {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteContravariantDefectCategoryᵒᵖ S.FiniteCovariantDefectCategory

Auslander's coherent dual as a contravariant functor from exact contravariant defects to exact covariant defects.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteCovariantDefectCategoryᵒᵖ (CategoryTheory.Functor S.IndecCategoryᵒᵖ (ModuleCat k))

The raw reverse coherent dual restricted to exact covariant defects.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsRaw_isLinear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantDefectCategoryᵒᵖ) : CoveringHom.IsLinearModule k (S.coherentCodualOnCovariantDefectsRaw.obj G)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsLinear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteCovariantDefectCategoryᵒᵖ (CoveringHom.LinearModuleCategory k)

The reverse coherent dual on exact covariant defects, valued in linear modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsLinear_isFiniteDimensional {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantDefectCategoryᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (S.coherentCodualOnCovariantDefectsLinear.obj G)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteCovariantDefectCategoryᵒᵖ S.FiniteContravariantFunctor

The reverse coherent dual restricted to exact covariant defects, valued in finite linear functors.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefectsFinite_isDefect {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantDefectCategoryᵒᵖ) : S.IsFiniteContravariantDefect (S.coherentCodualOnCovariantDefectsFinite.obj G)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefects {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : CategoryTheory.Functor S.FiniteCovariantDefectCategoryᵒᵖ S.FiniteContravariantDefectCategory

The reverse coherent dual as a contravariant functor from exact covariant defects to exact contravariant defects.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualOnContravariantDefects_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : S.coherentDualOnContravariantDefects.EssSurj

The coherent dual is essentially surjective on exact defects.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualOnCovariantDefects_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] [CategoryTheory.HasExt S.FiniteCovariantFunctor] : S.coherentCodualOnCovariantDefects.EssSurj

The reverse coherent dual is essentially surjective on exact defects.