The brick hypothesis for k(Γ_A) #
Lemma 5.2 (periodic-mesh-calculations.tex, the deletion brick lemma) for
C = k(Γ_A): by Proposition 2.10, C satisfies the hypotheses of the abstract
statement CatAlg.MeshData.brick (labels outside Σ of least evaluation
dimension have their radical endomorphisms factoring through Σ). In the
object quotient C/[Σ] the kernel on C(x, y) is the span of composites
through objects of Σ; hence such a label has endomorphism ring k in
C/[Σ].
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.objectQuotient_map_eq_zero_iff
{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)
(D : Set V)
{x y : V}
(f : obj c x ⟶ obj c y)
:
(RelationCategory.functor k (identityRelations c D)).map f = 0 ↔ f ∈ CatAlg.MeshData.through (fun (x : V) => obj c x) D x y
The kernel of C → C/[D] is the span of the composites through D.
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.brickHypothesis_of
{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))
(h :
∀ (D : Set V),
(∃ (x : V), x ∉ D) → ∃ x ∉ D, (localFamily c hfin).rad x x ≤ CatAlg.MeshData.through (fun (x : V) => obj c x) D x x)
:
The brick hypothesis follows from Lemma 5.2 in the form of
CatAlg.MeshData.brick.
theorem
MultiplicativeBasisDeformations.IndSkeleton.brickHypothesis
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
:
The brick hypothesis for k(Γ_A) (Lemma 5.2 with Proposition 2.10).