Exact meshes of a scalar mesh category and their descent to a prime field #
The mesh data of a scalar mesh category C(Q, c) (CatAlg.MeshData): the right mesh maps are
the arrows into each vertex, the left ones the coefficient-scaled mates, and the mesh sequences
are exact (MeshExact). For k(Γ_A) this is Proposition 2.6(1)(2) (IndSkeleton.arMeshData).
integral-deformations.tex: the prime-field model C⁽²⁾ inherits these properties
"since it does so after the faithful field extension to k". Here (MeshExact.descend):
exactness of the meshes of C(Q, c) over k, for a gauge c = η · (ι ∘ u) · μ μ, implies that of
C(Q, u) over the subfield K, through the form functor and its retractions (FormFunctor).
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.ScalarMeshCategory.qArr
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
(x : ↑Q.nonprojective)
(a : (y : V) × (y ⟶ ↑x))
:
The coefficient-scaled mate arrow c_{x,a} σa : τx → y.
Instances For
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.qArr_comp_zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
(x : ↑Q.nonprojective)
:
The mesh relation holds in C(Q, c).
structure
MultiplicativeBasisDeformations.ScalarMeshCategory.MeshExact
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
:
Exact meshes (Proposition 2.6(1)(2) for k(Γ_A)).
- cov_exact (x : ↑Q.nonprojective) (w : V) (g : (a : (y : V) × (y ⟶ ↑x)) → obj c w ⟶ obj c a.fst) : ∑ a : (y : V) × (y ⟶ ↑x), CategoryTheory.CategoryStruct.comp (g a) (arrowMor c a.snd) = 0 → ∃ (z : obj c w ⟶ obj c ↑(Q.tau x)), ∀ (a : (y : V) × (y ⟶ ↑x)), g a = CategoryTheory.CategoryStruct.comp z (qArr c x a)
- cov_mono (x : ↑Q.nonprojective) (w : V) (z : obj c w ⟶ obj c ↑(Q.tau x)) : (∀ (a : (y : V) × (y ⟶ ↑x)), CategoryTheory.CategoryStruct.comp z (qArr c x a) = 0) → z = 0
- contra_exact (x : ↑Q.nonprojective) (w : V) (v : (a : (y : V) × (y ⟶ ↑x)) → obj c a.fst ⟶ obj c w) : ∑ a : (y : V) × (y ⟶ ↑x), CategoryTheory.CategoryStruct.comp (qArr c x a) (v a) = 0 → ∃ (u : obj c ↑x ⟶ obj c w), ∀ (a : (y : V) × (y ⟶ ↑x)), v a = CategoryTheory.CategoryStruct.comp (arrowMor c a.snd) u
- contra_mono (x : ↑Q.nonprojective) (w : V) (u : obj c ↑x ⟶ obj c w) : (∀ (a : (y : V) × (y ⟶ ↑x)), CategoryTheory.CategoryStruct.comp (arrowMor c a.snd) u = 0) → u = 0
- proj_mono (x : V) : x ∉ Q.nonprojective → ∀ (w : V) (g : (a : (y : V) × (y ⟶ x)) → obj c w ⟶ obj c a.fst), ∑ a : (y : V) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (g a) (arrowMor c a.snd) = 0 → ∀ (a : (y : V) × (y ⟶ x)), g a = 0
Instances For
noncomputable def
MultiplicativeBasisDeformations.ScalarMeshCategory.meshDataOf
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
(hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y))
(hE : MeshExact c)
:
CatAlg.MeshData (fun (x : V) => obj c x) (localFamily c hfin)
The mesh data of a scalar mesh category with exact meshes.
Instances For
Descent along the form functor #
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.Fm_qArr
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq 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 : ↑Q.nonprojective)
(a : (y : V) × (y ⟶ ↑x))
:
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.MeshExact.descend
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq 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)
(hE : MeshExact c)
:
Exactness of the meshes descends to the subfield.