The additive-generator Auslander equivalence

For an object G in an idempotent-complete additive category, the representable functor Hom(G,-) identifies add(G) with the additive retract closure of the regular representable module Hom(G,G).

This is the exact generic foundation needed for Iyama's minimal realization in the magnitude campaign. It is a bounded adaptation of the corresponding core in the clean equidistribution formalization; no OP-conjecture module or classification layer is imported.

def MagnitudeConjecture.CategoryTheory.finiteAddClosure {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : CategoryTheory.ObjectProperty C

The object property add(G).

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_eq_top {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (hG : IsFiniteAddGenerator G) : finiteAddClosure G = ⊤

A finite additive generator has top additive closure.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteAddPresentation.replaceGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G H X : C} (e : G ≅ H) (P : FiniteAddPresentation G X) : FiniteAddPresentation H X

Replace the generator in a finite additive presentation by an isomorphic one.

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {G H X : C} (e : G ≅ H) : finiteAddClosure G X ↔ finiteAddClosure H X

The additive closure is invariant under isomorphic generators.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteAddPresentation.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G X Y : C} (P : FiniteAddPresentation G X) (Q : FiniteAddPresentation G Y) : FiniteAddPresentation G (X ⊞ Y)

Binary biproducts of objects in add(G) remain in add(G).

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G X Y : C} (hX : finiteAddClosure G X) (hY : finiteAddClosure G Y) : finiteAddClosure G (X ⊞ Y)

Object-property form of closure of add(G) under binary biproducts.

def MagnitudeConjecture.CategoryTheory.homFromGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : CategoryTheory.Functor (finiteAddClosure G).FullSubcategory (ModuleCat (CategoryTheory.End G)ᵐᵒᵖ)

The representable module functor on add(G). Mathlib uses left module categories, so the scalar ring is (End G)ᵐᵒᵖ.

theorem MagnitudeConjecture.CategoryTheory.exists_hom_of_moduleHom_of_finiteAddSource {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) {X Y : C} (P : FiniteAddPresentation G X) (α : ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ X) ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ Y)) : ∃ (f : X ⟶ Y), (CategoryTheory.preadditiveCoyonedaObj G).map f = α

A module map out of a representable object coming from add(G) is represented by a categorical morphism, even when the target object need not belong to add(G).

instance MagnitudeConjecture.CategoryTheory.homFromGenerator_full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : (homFromGenerator G).Full

Hom(G,-) is full on add(G).

instance MagnitudeConjecture.CategoryTheory.homFromGenerator_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : (homFromGenerator G).Faithful

Hom(G,-) is faithful on add(G).

noncomputable def MagnitudeConjecture.CategoryTheory.homFromGeneratorFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : (homFromGenerator G).FullyFaithful

Bundled full faithfulness of the representable functor on add(G).

def MagnitudeConjecture.CategoryTheory.regularLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : C) : (CategoryTheory.End G)ᵐᵒᵖ ≃ₗ[(CategoryTheory.End G)ᵐᵒᵖ] G ⟶ G

The regular left (End G)ᵐᵒᵖ-module is the self-representable module Hom(G,G).

theorem MagnitudeConjecture.CategoryTheory.homSelf_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : C) : CategoryTheory.Projective ((CategoryTheory.preadditiveCoyonedaObj G).obj G)

The self-representable module is projective over the opposite endomorphism ring.

noncomputable def MagnitudeConjecture.CategoryTheory.homFromGenerator_obj_finiteAddPresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) (X : (finiteAddClosure G).FullSubcategory) : FiniteAddPresentation ((CategoryTheory.preadditiveCoyonedaObj G).obj G) ((homFromGenerator G).obj X)

Every represented object from add(G) lies in the additive closure of the regular representable module.

def MagnitudeConjecture.CategoryTheory.homFromGeneratorToAdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : CategoryTheory.Functor (finiteAddClosure G).FullSubcategory (finiteAddClosure ((CategoryTheory.preadditiveCoyonedaObj G).obj G)).FullSubcategory

Hom(G,-) with its target restricted to the additive closure of the regular representable module.

noncomputable def MagnitudeConjecture.CategoryTheory.homFromGeneratorToAddFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) : (homFromGeneratorToAdd G).FullyFaithful

The target-restricted representable functor is fully faithful.

theorem MagnitudeConjecture.CategoryTheory.homFromGeneratorToAdd_essSurj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] (G : C) : (homFromGeneratorToAdd G).EssSurj

Idempotent completeness makes the target-restricted representable functor essentially surjective.

noncomputable def MagnitudeConjecture.CategoryTheory.additiveAuslanderEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] (G : C) : (finiteAddClosure G).FullSubcategory ≌ (finiteAddClosure ((CategoryTheory.preadditiveCoyonedaObj G).obj G)).FullSubcategory

The additive Auslander equivalence.

def MagnitudeConjecture.CategoryTheory.finiteProjectiveModules (R : Type v) [Ring R] : CategoryTheory.ObjectProperty (ModuleCat R)

The object property of finitely generated projective modules.

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_regular_iff (R : Type v) [Ring R] (M : ModuleCat R) : finiteAddClosure (ModuleCat.of R R) M ↔ finiteProjectiveModules R M

A module is a retract of a finite power of the regular module exactly when it is finitely generated and projective.

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_regular_eq_finiteProjective (R : Type v) [Ring R] : finiteAddClosure (ModuleCat.of R R) = finiteProjectiveModules R

The additive closure of the regular module is the finitely generated projective locus.

theorem MagnitudeConjecture.CategoryTheory.finiteAddClosure_homSelf_eq_finiteProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (G : C) : finiteAddClosure ((CategoryTheory.preadditiveCoyonedaObj G).obj G) = finiteProjectiveModules (CategoryTheory.End G)ᵐᵒᵖ

The additive closure of Hom(G,G) is the finitely generated projective module locus over (End G)ᵐᵒᵖ.

theorem MagnitudeConjecture.CategoryTheory.exists_obj_homSelf_iso_of_finite_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] (G : C) (M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ) (hM : finiteProjectiveModules (CategoryTheory.End G)ᵐᵒᵖ M) : ∃ (X : C), finiteAddClosure G X ∧ Nonempty ((CategoryTheory.preadditiveCoyonedaObj G).obj X ≅ M)

A finitely generated projective module over the opposite endomorphism ring is represented by an object of add(G).

noncomputable def MagnitudeConjecture.CategoryTheory.auslanderEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] (G : C) : (finiteAddClosure G).FullSubcategory ≌ (finiteProjectiveModules (CategoryTheory.End G)ᵐᵒᵖ).FullSubcategory

The additive Auslander equivalence with the conventional finitely generated projective target.

noncomputable def MagnitudeConjecture.CategoryTheory.finiteAddGeneratorAuslanderEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.IsIdempotentComplete C] (G : C) (hG : IsFiniteAddGenerator G) : C ≌ (finiteProjectiveModules (CategoryTheory.End G)ᵐᵒᵖ).FullSubcategory

If G generates the whole category, the source of the additive Auslander equivalence can be written as the ambient category.