Base change of scalar mesh categories along a field extension

integral-deformations.tex (Section 10): "The all-one meshes […] define a graded category C⁽²⁾ with k ⊗_{𝔽₂} C⁽²⁾ = C. […] Evaluation identifies C⁽²⁾ with their full Hom category, since it does so after the faithful field extension to k."

For a field extension K → k and coefficients u over K, extension of coefficients redE : C(Q, u) → C(Q, ι ∘ u) (ReductionMesh) is controlled by the coefficient retractions: for every K-linear θ : k → K, applying θ to the coefficients of path combinations (retP) maps the mesh ideal over k into the mesh ideal over K, so it descends to retE u θ : C(Q, ι ∘ u)(x, y) → C(Q, u)(x, y). It is a bimodule map over the morphisms coming from K (retE_comp_redE, retE_redE_comp) and retE u θ (λ • redE φ) = θ λ • φ. Consequently redE is injective, carries K-independent families to k-independent ones, its image spans, and the Hom spaces over K and k have the same dimension (finrank_redE).

noncomputable def MultiplicativeBasisDeformations.LinearPaths.retP {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y : V} : (obj x ⟶ obj y) →+ (obj x ⟶ obj y)

The coefficient retraction kQ → KQ along a K-linear map θ : k → K.

theorem MultiplicativeBasisDeformations.LinearPaths.retP_smul_path {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y : V} (t : k) (p : Quiver.Path x y) : (retP θ) (t • path p) = θ t • path p

theorem MultiplicativeBasisDeformations.LinearPaths.θ_mul_algebraMap {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] (θ : k →ₗ[K] K) (t : k) (a : K) : θ (t * (algebraMap K k) a) = a * θ t

theorem MultiplicativeBasisDeformations.LinearPaths.retP_smul_redP {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y : V} (t : k) (f : obj x ⟶ obj y) : (retP θ) (t • (redP (algebraMap K k)) f) = θ t • f

theorem MultiplicativeBasisDeformations.LinearPaths.retP_redP {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) (h1 : θ 1 = 1) {x y : V} (f : obj x ⟶ obj y) : (retP θ) ((redP (algebraMap K k)) f) = f

theorem MultiplicativeBasisDeformations.LinearPaths.retP_algSmul {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y : V} (a : K) (f : obj x ⟶ obj y) : (retP θ) ((algebraMap K k) a • f) = a • (retP θ) f

theorem MultiplicativeBasisDeformations.LinearPaths.retP_comp_redP {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y z : V} (g : obj x ⟶ obj y) (f : obj y ⟶ obj z) : (retP θ) (CategoryTheory.CategoryStruct.comp g ((redP (algebraMap K k)) f)) = CategoryTheory.CategoryStruct.comp ((retP θ) g) f

theorem MultiplicativeBasisDeformations.LinearPaths.retP_redP_comp {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] {V : Type v} [Quiver V] (θ : k →ₗ[K] K) {x y z : V} (f : obj x ⟶ obj y) (g : obj y ⟶ obj z) : (retP θ) (CategoryTheory.CategoryStruct.comp ((redP (algebraMap K k)) f) g) = CategoryTheory.CategoryStruct.comp f ((retP θ) g)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retP_mem_ideal {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} {g : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hg : g ∈ (RelSystem.mesh c).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) (t : k) : (LinearPaths.retP θ) (t • g) ∈ (RelSystem.mesh u).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

The retraction maps the mesh ideal over k into the mesh ideal over K.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.retE {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 : MeshCoefficients k Q} (θ : k →ₗ[K] K) {X Y : V} (φ : obj c X ⟶ obj c Y) : obj u X ⟶ obj u Y

The retraction on the scalar mesh category.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_map {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} (Φ : LinearPaths.obj X ⟶ LinearPaths.obj Y) : retE u θ ((RelationCategory.functor k (meshRelations c)).map Φ) = (RelationCategory.functor K (meshRelations u)).map ((LinearPaths.retP θ) Φ)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} (φ ψ : obj c X ⟶ obj c Y) : retE u θ (φ + ψ) = retE u θ φ + retE u θ ψ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} : retE u θ 0 = 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} (φ ψ : obj c X ⟶ obj c Y) : retE u θ (φ - ψ) = retE u θ φ - retE u θ ψ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} {ι : Type u_1} (s : Finset ι) (φ : ι → (obj c X ⟶ obj c Y)) : retE u θ (∑ i ∈ s, φ i) = ∑ i ∈ s, retE u θ (φ i)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_algSmul {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} (a : K) (φ : obj c X ⟶ obj c Y) : retE u θ ((algebraMap K k) a • φ) = a • retE u θ φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_smul_redE {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y : V} (t : k) (φ : obj u X ⟶ obj u Y) : retE u θ (t • redE (algebraMap K k) u c φ) = θ t • φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_redE {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) (h1 : θ 1 = 1) {X Y : V} (φ : obj u X ⟶ obj u Y) : retE u θ (redE (algebraMap K k) u c φ) = φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_comp_redE {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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y Z : V} (ψ : obj c X ⟶ obj c Y) (φ : obj u Y ⟶ obj u Z) : retE u θ (CategoryTheory.CategoryStruct.comp ψ (redE (algebraMap K k) u c φ)) = CategoryTheory.CategoryStruct.comp (retE u θ ψ) φ

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.retE_redE_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 : MeshCoefficients k Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a)) (θ : k →ₗ[K] K) {X Y Z : V} (φ : obj u X ⟶ obj u Y) (ψ : obj c Y ⟶ obj c Z) : retE u θ (CategoryTheory.CategoryStruct.comp (redE (algebraMap K k) u c φ) ψ) = CategoryTheory.CategoryStruct.comp φ (retE u θ ψ)

Consequences: injectivity, independence, spanning, dimension

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_retraction {K : Type} [Field K] {k : Type u} [Field k] [Algebra K k] : ∃ (θ : k →ₗ[K] K), θ 1 = 1

A K-linear retraction k → K of the scalars.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_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 : 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} : Function.Injective (redE (algebraMap K k) u c)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.linearIndependent_redE {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 : 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} {ι : Type u_1} {f : ι → (obj u X ⟶ obj u Y)} (hf : LinearIndependent K f) : LinearIndependent k fun (i : ι) => redE (algebraMap K k) u c (f i)

K-independent families stay independent over k.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.span_redE {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 : 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} : Submodule.span k (Set.range (redE (algebraMap K k) u c)) = ⊤

The image of redE spans.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.finiteDimensional_finrank_redE {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 : 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} [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: C(Q, u)(x, y) over K and C(Q, ι ∘ u)(x, y) over k.