Standardness in the independent vocabulary

Under translate compatibility, standardness of the corresponding skeleton in the proof library gives standardness of an independent family:

• the independent k(Γ_A) is equivalent to the all-one scalar mesh category (the two relation ideals agree);
• a gauge transformation (Lemma 4.4) identifies the all-one scalar mesh category with the one whose coefficients come from almost split sequences;
• the proof library supplies the equivalence of the latter with ind(mod A).

def MultiplicativeBasisDeformations.Statement.quotientComparison {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r s : HomRel C) (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), r f g ↔ s f g) : CategoryTheory.Functor (CategoryTheory.Quotient r) (CategoryTheory.Quotient s)

The identity of C induces a functor between quotients by relations with the same equivalent pairs.

theorem MultiplicativeBasisDeformations.Statement.quotientComparison_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r s : HomRel C) [CategoryTheory.Congruence r] [CategoryTheory.Congruence s] (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), r f g ↔ s f g) : (quotientComparison r s h).comp (quotientComparison s r ⋯) = CategoryTheory.Functor.id (CategoryTheory.Quotient r)

def MultiplicativeBasisDeformations.Statement.quotientEquivOfIff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (r s : HomRel C) [CategoryTheory.Congruence r] [CategoryTheory.Congruence s] (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), r f g ↔ s f g) : CategoryTheory.Quotient r ≌ CategoryTheory.Quotient s

Quotients by relations with the same equivalent pairs are equivalent.

@[reducible, inline]

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

The all-one scalar mesh category of Γ_A.

noncomputable def MultiplicativeBasisDeformations.Statement.toOneMesh {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) : MeshCategory S ≌ OneMesh S

The independent k(Γ_A) and the all-one scalar mesh category.

theorem MultiplicativeBasisDeformations.Statement.toOneMesh_linear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) : CategoryTheory.Functor.Linear k (toOneMesh hτ).functor

theorem MultiplicativeBasisDeformations.Statement.gaugeQ_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) {c : MeshCoefficients k (toSkeleton S).arTranslationQuiver} (μ : {x y : (toSkeleton S).ARVertex} → (x ⟶ y) → kˣ) (η : ↑(toSkeleton S).arTranslationQuiver.nonprojective → kˣ) (h : ∀ (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective) (y : (toSkeleton S).ARVertex) (a : y ⟶ ↑x), c x y a = η x * oneCoeff S x y a * μ (((toSkeleton S).arTranslationQuiver.mate x y) a) * μ a) : (ScalarMeshCategory.gaugeQ (fun {x y : (toSkeleton S).ARVertex} => μ) η (oneCoeff S) c h).IsEquivalence

Under the gauge c_{x,a} = η_x μ_{σa} μ_a from all-one coefficients, the gauge functor is an equivalence.

theorem MultiplicativeBasisDeformations.Statement.gaugeQ_linear {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) {c : MeshCoefficients k (toSkeleton S).arTranslationQuiver} (μ : {x y : (toSkeleton S).ARVertex} → (x ⟶ y) → kˣ) (η : ↑(toSkeleton S).arTranslationQuiver.nonprojective → kˣ) (h : ∀ (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective) (y : (toSkeleton S).ARVertex) (a : y ⟶ ↑x), c x y a = η x * oneCoeff S x y a * μ (((toSkeleton S).arTranslationQuiver.mate x y) a) * μ a) : CategoryTheory.Functor.Linear k (ScalarMeshCategory.gaugeQ (fun {x y : (toSkeleton S).ARVertex} => μ) η (oneCoeff S) c h)

theorem MultiplicativeBasisDeformations.Statement.linear_of_isLinearFunctor {k : Type u} [Field k] [IsAlgClosed k] {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] {F : CategoryTheory.Functor C D} (hF : IsLinearFunctor F) : CategoryTheory.Functor.Linear k F

A k-linear functor in the sense of the proof library is k-linear.

theorem MultiplicativeBasisDeformations.Statement.isStandardFor_of {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) (hstd : (toSkeleton S).IsStandard) : IsStandardFor S

Standardness in the independent vocabulary, from standardness of the corresponding skeleton in the proof library.