The independent translate is the translation of Γ_A

The independent statement defines τ X_i = X_t by an almost split sequence 0 → X_t → E → X_i → 0 of right modules, with the almost split properties tested on finite-dimensional modules. The proof library takes the translation from the vendored Auslander–Reiten theory: the kernel of the chosen minimal right almost split map in the category mod A = FGModuleCat Aᵐᵒᵖ of finitely generated right modules. This file proves that the two agree (translateCompatible).

• The inclusion mod A → Mod A is fully faithful and exact, so split monomorphisms and epimorphisms, almost split maps and short exact sequences correspond.
• The vendored sequence is an almost split sequence.
• Conversely, in an almost split sequence the first map is radical, so the second map is right minimal; uniqueness of minimal right almost split maps identifies the left term with the vendored translate.

theorem MultiplicativeBasisDeformations.Statement.isRightMinimal_g_of_shortExact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hf : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism S.f) : MBDVendor.QSE.IsRightMinimal S.g

In a short exact sequence with a radical first map, the second map is right minimal.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Statement.ιFG {A : Type u} [Ring A] : CategoryTheory.Functor (FGModuleCat Aᵐᵒᵖ) (ModuleCat Aᵐᵒᵖ)

The inclusion of finitely generated right modules into all right modules.

def MultiplicativeBasisDeformations.Statement.fgOf (k : Type u) {A : Type u} [Field k] [Ring A] [Algebra k A] (M : ModuleCat Aᵐᵒᵖ) (hM : Module.Finite k ↑M) : FGModuleCat Aᵐᵒᵖ

A finite-dimensional right module as a finitely generated one.

theorem MultiplicativeBasisDeformations.Statement.finite_of_fg (k : Type u) {A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (X : FGModuleCat Aᵐᵒᵖ) : Module.Finite k ↑(ιFG.obj X)

A finitely generated right module is finite-dimensional.

noncomputable def MultiplicativeBasisDeformations.Statement.homFG {A : Type u} [Ring A] {X Y : FGModuleCat Aᵐᵒᵖ} (f : ιFG.obj X ⟶ ιFG.obj Y) : X ⟶ Y

The preimage of a morphism of modules under the inclusion.

@[simp]

theorem MultiplicativeBasisDeformations.Statement.map_homFG {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FGModuleCat Aᵐᵒᵖ} (f : ιFG.obj X ⟶ ιFG.obj Y) : ιFG.map (homFG f) = f

theorem MultiplicativeBasisDeformations.Statement.isSplitMono_map_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) : CategoryTheory.IsSplitMono (ιFG.map f) ↔ CategoryTheory.IsSplitMono f

theorem MultiplicativeBasisDeformations.Statement.isSplitEpi_map_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) : CategoryTheory.IsSplitEpi (ιFG.map f) ↔ CategoryTheory.IsSplitEpi f

theorem MultiplicativeBasisDeformations.Statement.shortExact_map_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (T : CategoryTheory.ShortComplex (FGModuleCat Aᵐᵒᵖ)) : (T.map ιFG).ShortExact ↔ T.ShortExact

theorem MultiplicativeBasisDeformations.Statement.isAlmostSplitSequence_of_fg {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y Z : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) (hSE : { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := g, zero := w }.ShortExact) (hL : MBDVendor.QSE.IsLeftAlmostSplit f) (hR : MBDVendor.QSE.IsRightAlmostSplit g) : IsAlmostSplitSequence k (ιFG.map f) (ιFG.map g)

An almost split sequence of finitely generated modules is an almost split sequence of right modules in the independent sense.

theorem MultiplicativeBasisDeformations.Statement.fg_of_isAlmostSplitSequence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y Z : FGModuleCat Aᵐᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (h : IsAlmostSplitSequence k (ιFG.map f) (ιFG.map g)) : ∃ (w : CategoryTheory.CategoryStruct.comp f g = 0), { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := g, zero := w }.ShortExact ∧ ¬CategoryTheory.IsSplitMono f ∧ MBDVendor.QSE.IsRightAlmostSplit g

Conversely, an almost split sequence of right modules between finitely generated modules is short exact with a right almost split second map there.

theorem MultiplicativeBasisDeformations.Statement.isTranslate_tau {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective) : IsTranslate S ↑((toSkeleton S).arTranslationQuiver.tau x) ↑x

The vendored sequence ending at a nonprojective vertex is an almost split sequence in the independent sense.

theorem MultiplicativeBasisDeformations.Statement.exists_of_isTranslate {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) {t i : Vertex S} (h : IsTranslate S t i) : ∃ (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective), ↑x = i ∧ ↑((toSkeleton S).arTranslationQuiver.tau x) = t

An almost split sequence 0 → X_t → E → X_i → 0 forces X_i to be nonprojective and X_t to be its vendored translate.

theorem MultiplicativeBasisDeformations.Statement.translateCompatible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) : TranslateCompatible S

The independent translate is the translation of Γ_A.