The prime-field form of a scalar mesh category

integral-deformations.tex: "The all-one meshes […] define a graded category C⁽²⁾ with k ⊗_{𝔽₂} C⁽²⁾ = C." The coefficients of C = C(Q, c) are normalized to one by Lemma 4.4 (a gauge c_{x,a} = η_x μ_{σa} μ_a), and the all-one category over the prime field is a form of the all-one category over k.

Here: for coefficients u over a subfield K and a gauge c = η · (ι ∘ u) · μ μ over k, the form functor Fm = gauge ∘ redE : C(Q, u) → C(Q, c) (Fm), with Fm(a) = μ_a a on arrows, and for every K-linear θ : k → K the retraction Π θ = retE θ ∘ gauge⁻¹ : C(Q, c) → C(Q, u), a bimodule map over the image of Fm (Π_comp_Fm, Π_Fm_comp) with Π θ (t • Fm φ) = θ t • φ (Π_smul_Fm). Hence Fm is injective and the Hom spaces have equal dimensions (finrank_Fm).

The inverse gauge

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gauge_inv_rel {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x) : c x y a = (η x)⁻¹ * c' x y a * (μ ((Q.mate x y) a))⁻¹ * (μ a)⁻¹

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeInv {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) : CategoryTheory.Functor (ScalarMeshCategory k Q c') (ScalarMeshCategory k Q c)

The inverse gauge functor C(Q, c') → C(Q, c).

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathWt_inv {k : Type u} [Field k] {V : Type v} [Quiver V] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y : V} (p : Quiver.Path x y) : pathWt (fun {x x_1 : V} (a : x ⟶ x_1) => (μ a)⁻¹) p = (pathWt (fun {x y : V} => μ) p)⁻¹

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeInv_gaugeQ {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (φ : obj c x ⟶ obj c y) : (gaugeInv (fun {x y : V} => μ) η c c' h).map ((gaugeQ (fun {x y : V} => μ) η c c' h).map φ) = φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeQ_gaugeInv {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (ψ : obj c' x ⟶ obj c' y) : (gaugeQ (fun {x y : V} => μ) η c c' h).map ((gaugeInv (fun {x y : V} => μ) η c c' h).map ψ) = ψ

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.gaugeEquiv {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (x y : V) : (obj c x ⟶ obj c y) ≃ₗ[k] obj c' x ⟶ obj c' y

The gauge, as a linear equivalence of Hom spaces.

The form functor and its retractions

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.Fm {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (φ : obj u x ⟶ obj u y) : obj c x ⟶ obj c y

The form functor C(Q, u) → C(Q, c) on morphisms.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.retF {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y : V} (ψ : obj c x ⟶ obj c y) : obj u x ⟶ obj u y

The retraction C(Q, c) → C(Q, u) along θ.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_comp {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y z : V} (φ : obj u x ⟶ obj u y) (φ' : obj u y ⟶ obj u z) : Fm u c₁ c (fun {x y : V} => μ) η h (CategoryTheory.CategoryStruct.comp φ φ') = CategoryTheory.CategoryStruct.comp (Fm u c₁ c (fun {x y : V} => μ) η h φ) (Fm u c₁ c (fun {x y : V} => μ) η h φ')

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_add {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (φ φ' : obj u x ⟶ obj u y) : Fm u c₁ c (fun {x y : V} => μ) η h (φ + φ') = Fm u c₁ c (fun {x y : V} => μ) η h φ + Fm u c₁ c (fun {x y : V} => μ) η h φ'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_zero {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} : Fm u c₁ c (fun {x y : V} => μ) η h 0 = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_smul {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (a : K) (φ : obj u x ⟶ obj u y) : Fm u c₁ c (fun {x y : V} => μ) η h (a • φ) = (algebraMap K k) a • Fm u c₁ c (fun {x y : V} => μ) η h φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_sub {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (φ φ' : obj u x ⟶ obj u y) : Fm u c₁ c (fun {x y : V} => μ) η h (φ - φ') = Fm u c₁ c (fun {x y : V} => μ) η h φ - Fm u c₁ c (fun {x y : V} => μ) η h φ'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_sum {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} {ι : Type u_1} (s : Finset ι) (φ : ι → (obj u x ⟶ obj u y)) : Fm u c₁ c (fun {x y : V} => μ) η h (∑ i ∈ s, φ i) = ∑ i ∈ s, Fm u c₁ c (fun {x y : V} => μ) η h (φ i)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_arrowMor {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} (a : x ⟶ y) : Fm u c₁ c (fun {x y : V} => μ) η h (arrowMor u a) = ↑(μ a) • arrowMor c a

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_id {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (x : V) : Fm u c₁ c (fun {x y : V} => μ) η h (CategoryTheory.CategoryStruct.id (obj u x)) = CategoryTheory.CategoryStruct.id (obj c x)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_add {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y : V} (ψ ψ' : obj c x ⟶ obj c y) : retF u c₁ c (fun {x y : V} => μ) η h θ (ψ + ψ') = retF u c₁ c (fun {x y : V} => μ) η h θ ψ + retF u c₁ c (fun {x y : V} => μ) η h θ ψ'

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_zero {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y : V} : retF u c₁ c (fun {x y : V} => μ) η h θ 0 = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_sum {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y : V} {ι : Type u_1} (s : Finset ι) (ψ : ι → (obj c x ⟶ obj c y)) : retF u c₁ c (fun {x y : V} => μ) η h θ (∑ i ∈ s, ψ i) = ∑ i ∈ s, retF u c₁ c (fun {x y : V} => μ) η h θ (ψ i)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_smul_Fm {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y : V} (t : k) (φ : obj u x ⟶ obj u y) : retF u c₁ c (fun {x y : V} => μ) η h θ (t • Fm u c₁ c (fun {x y : V} => μ) η h φ) = θ t • φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_Fm {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) (h1 : θ 1 = 1) {x y : V} (φ : obj u x ⟶ obj u y) : retF u c₁ c (fun {x y : V} => μ) η h θ (Fm u c₁ c (fun {x y : V} => μ) η h φ) = φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_comp_Fm {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y z : V} (ψ : obj c x ⟶ obj c y) (φ : obj u y ⟶ obj u z) : retF u c₁ c (fun {x y : V} => μ) η h θ (CategoryTheory.CategoryStruct.comp ψ (Fm u c₁ c (fun {x y : V} => μ) η h φ)) = CategoryTheory.CategoryStruct.comp (retF u c₁ c (fun {x y : V} => μ) η h θ ψ) φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retF_Fm_comp {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) (θ : k →ₗ[K] K) {x y z : V} (φ : obj u x ⟶ obj u y) (ψ : obj c y ⟶ obj c z) : retF u c₁ c (fun {x y : V} => μ) η h θ (CategoryTheory.CategoryStruct.comp (Fm u c₁ c (fun {x y : V} => μ) η h φ) ψ) = CategoryTheory.CategoryStruct.comp φ (retF u c₁ c (fun {x y : V} => μ) η h θ ψ)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_injective {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} : Function.Injective (Fm u c₁ c (fun {x y : V} => μ) η h)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.finiteDimensional_finrank_Fm {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients K Q) (c₁ c : MeshCoefficients k Q) (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c₁ x y a)) (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c x y a = η x * c₁ x y a * μ ((Q.mate x y) a) * μ a) {x y : V} [FiniteDimensional k (obj c x ⟶ obj c y)] : FiniteDimensional K (obj u x ⟶ obj u y) ∧ Module.finrank K (obj u x ⟶ obj u y) = Module.finrank k (obj c x ⟶ obj c y)

Equal dimensions.