Bridge to the vendored Auslander--Reiten theory

The vendored library MBDVendor (general Auslander--Reiten theory, copied from the magnitude-conjecture formalization) works with finitely generated right modules FGModuleCat Aᵐᵒᵖ and with the radical of that whole category. This file connects it with the manuscript-literal objects of Foundations/RightModules.lean:

• an IndSkeleton is a vendored FiniteIndecomposableSkeleton;
• ind(mod A) embeds fully faithfully into mod A = FGModuleCat Aᵐᵒᵖ;
• the radical morphisms of ind(mod A) are the vendored radical morphisms;
• J²(X, Y), defined through indecomposable intermediate objects, is the vendored radical square, defined through arbitrary finitely generated intermediate modules;
• hence Irr(X, Y) is linearly isomorphic to the vendored irreducible space.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ModCat (A : Type u) [Ring A] : Type (u + 1)

mod A: finitely generated right A-modules.

theorem MultiplicativeBasisDeformations.comp_eq_sum_biproduct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {ι : Type} [Fintype ι] {F : ι → C} [CategoryTheory.Limits.HasBiproduct F] {X M Y : C} (e : M ≅ ⨁ F) (a : X ⟶ M) (b : M ⟶ Y) : CategoryTheory.CategoryStruct.comp a b = ∑ i : ι, CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.biproduct.π F i))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι F i) (CategoryTheory.CategoryStruct.comp e.inv b))

A composite through an object with a finite biproduct decomposition is the sum of the composites through the summands.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.toVendor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton k A

An indecomposable skeleton, as a skeleton of the vendored library.

@[simp]

theorem MultiplicativeBasisDeformations.IndSkeleton.toVendor_n {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : S.toVendor.n = S.n

@[simp]

theorem MultiplicativeBasisDeformations.IndSkeleton.toVendor_obj {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (i : Fin S.n) : S.toVendor.obj i = S.obj i

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.fg {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : ModCat A

The object of mod A labelled by an index.

def MultiplicativeBasisDeformations.IndSkeleton.toFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : CategoryTheory.Functor S.Ind (ModCat A)

The full embedding ind(mod A) → mod A.

instance MultiplicativeBasisDeformations.IndSkeleton.instFullIndModCatToFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : S.toFG.Full

instance MultiplicativeBasisDeformations.IndSkeleton.instFaithfulIndModCatToFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : S.toFG.Faithful

instance MultiplicativeBasisDeformations.IndSkeleton.instAdditiveIndModCatToFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : S.toFG.Additive

instance MultiplicativeBasisDeformations.IndSkeleton.instLinearIndModCatToFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : CategoryTheory.Functor.Linear k S.toFG

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.homEquivFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : (X ⟶ Y) ≃ₗ[k] S.toFG.obj X ⟶ S.toFG.obj Y

ind(mod A) → mod A on Hom spaces, as a k-linear equivalence.

@[simp]

theorem MultiplicativeBasisDeformations.IndSkeleton.homEquivFG_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (f : X ⟶ Y) : (S.homEquivFG X Y) f = S.toFG.map f

theorem MultiplicativeBasisDeformations.IndSkeleton.isRadical_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (f : X ⟶ Y) : S.IsRadical f ↔ MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism (S.toFG.map f)

A morphism of ind(mod A) is radical exactly when its image in mod A is a radical morphism in the sense of the vendored library.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_one_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (f : X ⟶ Y) : f ∈ S.radPow 1 X Y ↔ S.IsRadical f

J(X, Y) consists exactly of the radical morphisms.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.vendorRadicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : AddSubgroup (S.toFG.obj X ⟶ S.toFG.obj Y)

The radical square of the vendored library: the additive subgroup generated by composites of two radical morphisms through arbitrary objects of mod A.

theorem MultiplicativeBasisDeformations.IndSkeleton.map_homEquivFG_symm {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y : S.Ind} (g : S.toFG.obj X ⟶ S.toFG.obj Y) : S.toFG.map ((S.homEquivFG X Y).symm g) = g

Mapping back and forth along the embedding into mod A.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_two_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : S.Ind} (f : X ⟶ Y) : f ∈ S.radPow 2 X Y ↔ S.toFG.map f ∈ S.vendorRadicalSquare X Y

J²(X, Y), defined through indecomposable intermediate objects, is the vendored radical square, defined through arbitrary finitely generated intermediate modules.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.vendorIrr {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : Type u

The vendored intrinsic irreducible space rad(X, Y) / rad²(X, Y) of mod A, at two labelled indecomposables.

theorem MultiplicativeBasisDeformations.IndSkeleton.radPow_one_map_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : Submodule.map (↑(S.homEquivFG X Y)) (S.radPow 1 X Y) = MBDVendor.Magnitude.CategoricalIrreducible.radical k (S.toFG.obj X) (S.toFG.obj Y)

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.radPowOneEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : ↥(S.radPow 1 X Y) ≃ₗ[k] ↥(MBDVendor.Magnitude.CategoricalIrreducible.radical k (S.toFG.obj X) (S.toFG.obj Y))

J(X, Y) and the vendored radical, as linearly equivalent spaces.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.irrEquivVendor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X Y : S.Ind) : S.Irr X Y ≃ₗ[k] S.vendorIrr X Y

Irr(X, Y) is linearly isomorphic to the vendored irreducible space.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_eq_vendor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X Y : S.Ind) : Module.finrank k (S.Irr X Y) = Module.finrank k (S.vendorIrr X Y)