Proposition 2.6(3): k(Γ_A) is the radical grading of ind(mod A) #
graded-category.tex. Sending each arrow to its chosen class in
C_1 = Irr defines a functor from the path category; it kills each mesh
relation, because the degree-two part of p ∘ i = 0 is the image of r_Y;
the resulting graded functor k(Γ_A) → gr_J ind(mod A) is surjective because
the radical layers are generated in degree one, and injective by induction on
the degree, using the exactness of Proposition 2.6(1).
Formally, choose for each arrow a : x → y a representative rep a ∈ J(x, y)
of the chosen basis vector of Irr(x, y). A path is realized by the composite
of the representatives (pathMap), and a morphism of kQ by linear extension
(realize). A path of length d lands in J^d, so a homogeneous morphism of
degree d has a class in the radical layer J^d/J^{d+1}.
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.rep
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{x y : S.ARVertex}
(a : x ⟶ y)
:
A representative in J(x, y) of the basis vector of Irr(x, y) indexed by
the arrow a.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.rep_mem
{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)
{x y : S.ARVertex}
(a : x ⟶ y)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.irrClass_rep
{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)
{x y : S.ARVertex}
(a : x ⟶ y)
:
def
MultiplicativeBasisDeformations.IndSkeleton.pathMap
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{x y : S.ARVertex}
:
The realization of a path: the composite of the representatives of its arrows.
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.IndSkeleton.pathMap_nil
{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)
{x : S.ARVertex}
:
@[simp]
theorem
MultiplicativeBasisDeformations.IndSkeleton.pathMap_cons
{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)
{x y z : S.ARVertex}
(p : Quiver.Path x y)
(a : y ⟶ z)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.pathMap_comp
{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)
{x y z : S.ARVertex}
(p : Quiver.Path x y)
(q : Quiver.Path y z)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.pathMap_mem
{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)
{x y : S.ARVertex}
(p : Quiver.Path x y)
:
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.realize
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
(S : IndSkeleton k A)
(b : S.ArrowBases)
(x y : S.ARVertex)
:
(LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] S.label x ⟶ S.label y
The realization of a morphism of kQ, by linear extension.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_path
{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)
{x y : S.ARVertex}
(p : Quiver.Path x y)
:
(S.realize b x y) (LinearPaths.path p) = S.pathMap b p
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_comp
{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)
{x y z : S.ARVertex}
(f : LinearPaths.obj x ⟶ LinearPaths.obj y)
(g : LinearPaths.obj y ⟶ LinearPaths.obj z)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_mem
{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)
{d : ℕ}
{x y : S.ARVertex}
{f : LinearPaths.obj x ⟶ LinearPaths.obj y}
(hf : f ∈ LinearPaths.degreePart d x y)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.eq_repr_smul_basis
{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)
{x y : S.ARVertex}
(a : x ⟶ y)
(v : S.Irr (S.label x) (S.label y))
:
v = ((b x y).repr v) a • (b x y) a
In Irr(x, y), every vector is a multiple of the basis vector of the
(unique) arrow.
theorem
MultiplicativeBasisDeformations.IndSkeleton.sub_repr_smul_rep_mem
{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)
{x y : S.ARVertex}
(a : x ⟶ y)
{f : S.label x ⟶ S.label y}
(hf : f ∈ S.radPow 1 (S.label x) (S.label y))
:
A radical map agrees modulo J² with the corresponding multiple of the
representative of the arrow.
theorem
MultiplicativeBasisDeformations.IndSkeleton.sum_source_beta
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
:
∑ i :
Fin
(MBDVendor.Magnitude.FiniteTauMatrix.rightMiddleArity S.tau.toFiniteRightTauCategoryData
↑(S.vendorNonprojective x)),
CategoryTheory.CategoryStruct.comp
(MBDVendor.Magnitude.FiniteTauMatrix.rightMiddleSourceComponent S.tau (S.vendorNonprojective x) i)
(S.beta (S.index ↑x) i) = 0
The components of the canonical mesh at a nonprojective vertex compose to
zero: ∑_i α_i β_i = 0.
theorem
MultiplicativeBasisDeformations.IndSkeleton.comp_sub_comp_mem_three
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
(S : IndSkeleton k A)
{X Y Z : S.Ind}
{f f₀ : X ⟶ Y}
{g g₀ : Y ⟶ Z}
(hf : f - f₀ ∈ S.radPow 2 X Y)
(hf₀ : f₀ ∈ S.radPow 1 X Y)
(hg : g - g₀ ∈ S.radPow 2 Y Z)
(hg₀ : g₀ ∈ S.radPow 1 Y Z)
:
CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f₀ g₀ ∈ S.radPow 3 X Z
Agreement modulo J² of two radical factors gives agreement modulo J³
of their composites.
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.alphaInd
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
S.label ↑(S.arTranslationQuiver.tau x) ⟶ S.label y
The component τx → y at an occurrence, in ind(mod A).
Instances For
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.betaInd
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
The component y → x at an occurrence, in ind(mod A).
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.alphaInd_mem
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.betaInd_mem
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.occurrence_term_mem
{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)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(a : y ⟶ ↑x)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
CategoryTheory.CategoryStruct.comp (S.alphaInd x y i) (S.betaInd x y i) - S.occurrenceCoefficient b x y a i • CategoryTheory.CategoryStruct.comp (S.rep b ((S.arTranslationQuiver.mate x y) a)) (S.rep b a) ∈ S.radPow 3 (S.label ↑(S.arTranslationQuiver.tau x)) (S.label ↑x)
One occurrence contributes u_i v_i (σ a) a modulo J³.
theorem
MultiplicativeBasisDeformations.IndSkeleton.sourceComponent_comp_occurrenceMap
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
{y : Fin S.n}
(i : S.toVendor.Occurrence y (S.index ↑x))
:
CategoryTheory.CategoryStruct.comp (S.sourceComponent x i) (S.toVendor.occurrenceMap i) = CategoryTheory.CategoryStruct.comp
(MBDVendor.Magnitude.FiniteTauMatrix.rightMiddleSourceComponent S.tau (S.vendorNonprojective x) ↑i)
(S.beta (S.index ↑x) ↑i)
theorem
MultiplicativeBasisDeformations.IndSkeleton.alphaInd_comp_betaInd
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
(y : S.ARVertex)
(i : S.toVendor.Occurrence (S.index y) (S.index ↑x))
:
CategoryTheory.CategoryStruct.comp (S.alphaInd x y i) (S.betaInd x y i) = (S.homEquivFG (S.ind (S.index ↑(S.arTranslationQuiver.tau x))) (S.ind (S.index ↑x))).symm
(CategoryTheory.CategoryStruct.comp
(MBDVendor.Magnitude.FiniteTauMatrix.rightMiddleSourceComponent S.tau (S.vendorNonprojective x) ↑i)
(S.beta (S.index ↑x) ↑i))
theorem
MultiplicativeBasisDeformations.IndSkeleton.sum_alphaInd_betaInd
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : ↑S.nonprojectiveVertices)
:
The sum of the occurrence composites at a vertex vanishes.
theorem
MultiplicativeBasisDeformations.IndSkeleton.card_arrows_eq_card_occurrence
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x y : S.ARVertex)
:
Fintype.card (y ⟶ x) = Fintype.card (S.toVendor.Occurrence (S.index y) (S.index x))
The number of arrows y → x equals the number of occurrences of y in
the mesh ending at x.
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_meshRelation_mem
{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)
(x : ↑S.nonprojectiveVertices)
:
(S.realize b ↑(S.arTranslationQuiver.tau x) ↑x) (meshRelation (S.arCoefficients b) x) ∈ S.radPow 3 (S.label ↑(S.arTranslationQuiver.tau x)) (S.label ↑x)
The mesh relations are realized in J³: the degree-two part of
p ∘ i = 0 is the image of r_x.
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_proj_mem_of_mem_ideal
{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)
(d : ℕ)
{x y : S.ARVertex}
{g : LinearPaths.obj x ⟶ LinearPaths.obj y}
(hg :
g ∈ (CategoricalIdeal.HomIdeal.linearSpan k (meshRelations (S.arCoefficients b))).hom (LinearPaths.obj x)
(LinearPaths.obj y))
:
(S.realize b x y) ((LinearPaths.proj d x y) g) ∈ S.radPow (d + 1) (S.label x) (S.label y)
The degree-d component of an element of the mesh ideal is realized in
J^{d+1}.
theorem
MultiplicativeBasisDeformations.IndSkeleton.isRadical_of_ne
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
{x y : Fin S.n}
(hxy : x ≠ y)
(f : S.ind x ⟶ S.ind y)
:
S.IsRadical f
Maps between distinct (hence nonisomorphic) indecomposables are radical.
theorem
MultiplicativeBasisDeformations.IndSkeleton.exists_sub_smul_id_isRadical
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : Fin S.n)
(f : S.ind x ⟶ S.ind x)
:
An endomorphism of an indecomposable is a scalar plus a radical map.
theorem
MultiplicativeBasisDeformations.IndSkeleton.exists_realize_sub_mem
{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)
(d : ℕ)
{x y : S.ARVertex}
(f : S.label x ⟶ S.label y)
:
Surjectivity in Proposition 2.6(3): the radical layers are generated in
degree one. Every f ∈ J^d agrees modulo J^{d+1} with the realization of a
homogeneous morphism of degree d of the path category.
theorem
MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_eq_card_occurrence
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x y : Fin S.n)
:
Module.finrank k (S.Irr (S.ind x) (S.ind y)) = Fintype.card (S.toVendor.Occurrence x y)
dim Irr(x, y) is the number of occurrences of x in the middle term of the
mesh ending at y.
def
MultiplicativeBasisDeformations.IndSkeleton.occArrow
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
The arrow E_i → Y given by a summand i of the middle term of the mesh
ending at Y.
Instances For
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.occEquiv
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
:
The summands of the middle term at Y correspond bijectively to the arrows
ending at Y.
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.IndSkeleton.occEquiv_apply_fst
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.betaI
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
The component β_i of the right almost split map, in ind(mod A).
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.betaI_mem
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.vCoeff
{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)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
k
The coordinate v_i of β_i in the arrow basis; it is nonzero.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.vCoeff_ne_zero
{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)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
S.vCoeff b Y i ≠ 0
theorem
MultiplicativeBasisDeformations.IndSkeleton.betaI_sub_mem
{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)
(Y : S.ARVertex)
(i : Fin (S.arity (S.index Y)))
:
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.alphaI
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
The component α_i : τY → E_i of the first map, in ind(mod A).
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.alphaI_mem
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.uCoeff
{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)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
k
The coordinate u_i of α_i in the arrow basis.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.alphaI_sub_mem
{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)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.arCoefficients_occArrow
{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)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
The mesh coefficient of the arrow of the summand i is u_i v_i.
theorem
MultiplicativeBasisDeformations.IndSkeleton.isZero_rightMesh_X₁_of_not_mem
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(Y : S.ARVertex)
(hY : Y ∉ S.nonprojectiveVertices)
:
At a projective vertex the first term of the mesh is zero.
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.IndSkeleton.meshIdeal
{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 mesh ideal of k(Γ_A) in the linear path category.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.not_isRadical_id
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(x : S.Ind)
:
¬S.IsRadical (CategoryTheory.CategoryStruct.id x)
The identity of an indecomposable is not radical.
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_arrow
{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)
{x y : S.ARVertex}
(a : x ⟶ y)
:
(S.realize b x y) (LinearPaths.arrow a) = S.rep b a
theorem
MultiplicativeBasisDeformations.IndSkeleton.sum_lastArrow_eq
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
{W Y : S.ARVertex}
{M : Type u_1}
[AddCommMonoid M]
(Φ : (X : S.ARVertex) × (X ⟶ Y) → M)
:
Reindexing the last-arrow decomposition by the summands of the mesh.
theorem
MultiplicativeBasisDeformations.IndSkeleton.inv_smul_comp_sub_aux
{k A : Type w}
[Field k]
[Ring A]
[Algebra k A]
(S : IndSkeleton k A)
{X Y Z : S.Ind}
(g : X ⟶ Y)
(β r : Y ⟶ Z)
{v : k}
(hv : v ≠ 0)
:
CategoryTheory.CategoryStruct.comp (v⁻¹ • g) β - CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp (v⁻¹ • g) (β - v • r)
theorem
MultiplicativeBasisDeformations.IndSkeleton.sum_inv_v_betaI_mem
{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)
{N : ℕ}
{W Y : S.ARVertex}
(G : (a : (X : S.ARVertex) × (X ⟶ Y)) → LinearPaths.obj W ⟶ LinearPaths.obj a.fst)
(hG : ∀ (a : (X : S.ARVertex) × (X ⟶ Y)), G a ∈ LinearPaths.degreePart N W a.fst)
(hF :
(S.realize b W Y)
(∑ a : (X : S.ARVertex) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp (G a) (LinearPaths.arrow a.snd)) ∈ S.radPow (N + 2) (S.label W) (S.label Y))
:
The estimate ∑_i v_i⁻¹ G_i β_i ∈ J^{N+2} used in the injectivity step.
theorem
MultiplicativeBasisDeformations.IndSkeleton.alphaI_map
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
:
S.toFG.map (S.alphaI y i) = CategoryTheory.CategoryStruct.comp (S.tau.tauPlusIso (S.vendorNonprojective y)).inv
(CategoryTheory.CategoryStruct.comp (S.rightMesh (S.index ↑y)).f (S.midProj (S.index ↑y) i))
theorem
MultiplicativeBasisDeformations.IndSkeleton.realize_corrected_mem
{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)
{m : ℕ}
{W : S.ARVertex}
(y : ↑S.nonprojectiveVertices)
(i : Fin (S.arity (S.index ↑y)))
(Gi : LinearPaths.obj W ⟶ LinearPaths.obj (S.vertex (S.midLabel (S.index ↑y) i)))
(H : LinearPaths.obj W ⟶ LinearPaths.obj ↑(S.arTranslationQuiver.tau y))
(hH : H ∈ LinearPaths.degreePart m W ↑(S.arTranslationQuiver.tau y))
(hInd : S.label W ⟶ S.label ↑(S.arTranslationQuiver.tau y))
(hHdiff :
hInd - (S.realize b W ↑(S.arTranslationQuiver.tau y)) H ∈ S.radPow (m + 1) (S.label W) (S.label ↑(S.arTranslationQuiver.tau y)))
(h1 :
(S.vCoeff b (↑y) i)⁻¹ • (S.realize b W (S.vertex (S.midLabel (S.index ↑y) i))) Gi - CategoryTheory.CategoryStruct.comp hInd (S.alphaI y i) ∈ S.radPow (m + 2) (S.label W) (S.label (S.vertex (S.midLabel (S.index ↑y) i))))
:
(S.realize b W (S.vertex (S.midLabel (S.index ↑y) i)))
(Gi - ↑(S.arCoefficients b y (S.vertex (S.midLabel (S.index ↑y) i)) (S.occArrow (↑y) i)) • CategoryTheory.CategoryStruct.comp H
(LinearPaths.arrow
((S.arTranslationQuiver.mate y (S.vertex (S.midLabel (S.index ↑y) i))) (S.occArrow (↑y) i)))) ∈ S.radPow (m + 2) (S.label W) (S.label (S.vertex (S.midLabel (S.index ↑y) i)))
The corrected component G_i - c_i H (σ a_i) is realized in J^{m+2}.
theorem
MultiplicativeBasisDeformations.IndSkeleton.lastArrow_sum_mem_of
{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)
{W Y : S.ARVertex}
(G : (a : (X : S.ARVertex) × (X ⟶ Y)) → LinearPaths.obj W ⟶ LinearPaths.obj a.fst)
(hG :
∀ (i : Fin (S.arity (S.index Y))),
G ⟨S.vertex (S.midLabel (S.index Y) i), S.occArrow Y i⟩ ∈ (S.meshIdeal b).hom (LinearPaths.obj W)
(LinearPaths.obj ⟨S.vertex (S.midLabel (S.index Y) i), S.occArrow Y i⟩.fst))
:
∑ a : (X : S.ARVertex) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp (G a) (LinearPaths.arrow a.snd) ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj Y)
theorem
MultiplicativeBasisDeformations.IndSkeleton.mem_meshIdeal_of_realize_mem
{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)
(N : ℕ)
{W Y : S.ARVertex}
{F : LinearPaths.obj W ⟶ LinearPaths.obj Y}
:
F ∈ LinearPaths.degreePart N W Y →
(S.realize b W Y) F ∈ S.radPow (N + 1) (S.label W) (S.label Y) →
F ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj Y)
Injectivity in Proposition 2.6(3): a homogeneous morphism of degree N
of the path category whose realization lies in J^{N+1} belongs to the mesh
ideal.