Proposition 2.6(3), assembled #
The realization of the path category on radical layers descends to linear
isomorphisms φ_d : C_d(x, y) ≃ J^d/J^{d+1} from the path-degree parts of
k(Γ_A) = C(Γ_A, c) (GradedRealization.lean: well-definedness from the
mesh relations, surjectivity, injectivity). They send arrows to the chosen
basis vectors and are compatible with composition. The Hom spaces of
k(Γ_A) are the internal direct sums of their degree parts, because the mesh
ideal is generated by homogeneous relations.
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.IndSkeleton.meshQuot
{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)
:
CategoryTheory.Functor (LinearPaths k S.ARVertex) (RelationCategory k (meshRelations (S.arCoefficients b)))
The quotient functor kQ → k(Γ_A).
Instances For
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.IndSkeleton.meshQuotL
{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)
:
(LinearPaths.obj x ⟶ LinearPaths.obj y) →ₗ[k] (S.meshQuot b).obj (LinearPaths.obj x) ⟶ (S.meshQuot b).obj (LinearPaths.obj y)
The quotient map on Hom spaces.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.meshQuot_map_eq_zero_iff
{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}
(F : LinearPaths.obj x ⟶ LinearPaths.obj y)
:
(S.meshQuot b).map F = 0 ↔ F ∈ (S.meshIdeal b).hom (LinearPaths.obj x) (LinearPaths.obj y)
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.IndSkeleton.qd
{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)
:
↥(LinearPaths.degreePart d x y) →ₗ[k] ↥(Submodule.map (S.meshQuotL b x y) (LinearPaths.degreePart d x y))
The quotient map restricted to degree d.
Instances For
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.psi
{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)
:
↥(LinearPaths.degreePart d x y) →ₗ[k] S.layer d (S.label x) (S.label y)
The realization on degree d, followed by the class in J^d/J^{d+1}.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.psi_eq_zero_iff
{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.degreePart d x y))
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.ker_qd_eq_ker_psi
{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)
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.psi_surjective
{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)
:
Function.Surjective ⇑(S.psi b d x y)
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.phi
{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)
:
↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) ≃ₗ[k] S.layer d (S.label x) (S.label y)
φ_d : C_d(x, y) ≃ J^d/J^{d+1}.
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.phi_qd
{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.degreePart d x y))
:
theorem
MultiplicativeBasisDeformations.IndSkeleton.meshQuotL_surjective
{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)
:
Function.Surjective ⇑(S.meshQuotL b x y)
theorem
MultiplicativeBasisDeformations.IndSkeleton.ker_meshQuotL_le
{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)
:
(S.meshQuotL b x y).ker ≤ (S.meshQuotL b x y ∘ₗ LinearPaths.proj d x y).ker
noncomputable def
MultiplicativeBasisDeformations.IndSkeleton.meshProj
{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)
:
((S.meshQuot b).obj (LinearPaths.obj x) ⟶ (S.meshQuot b).obj (LinearPaths.obj y)) →ₗ[k] (S.meshQuot b).obj (LinearPaths.obj x) ⟶ (S.meshQuot b).obj (LinearPaths.obj y)
The degree-d projection on the Hom spaces of k(Γ_A).
Instances For
theorem
MultiplicativeBasisDeformations.IndSkeleton.meshProj_apply
{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)
:
(S.meshProj b d x y) ((S.meshQuot b).map F) = (S.meshQuot b).map ((LinearPaths.proj d x y) F)
theorem
MultiplicativeBasisDeformations.IndSkeleton.isInternal_degreePart
{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)
:
DirectSum.IsInternal fun (d : ℕ) => ScalarMeshCategory.degreePart (S.arCoefficients b) d x y
The Hom spaces of k(Γ_A) are the internal direct sums of their path-degree
parts.
theorem
MultiplicativeBasisDeformations.IndSkeleton.phi_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)
(ha : ScalarMeshCategory.arrowMor (S.arCoefficients b) a ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) 1 x y)
:
(S.phi b 1 x y) ⟨ScalarMeshCategory.arrowMor (S.arCoefficients b) a, ha⟩ = (b x y) a
theorem
MultiplicativeBasisDeformations.IndSkeleton.phi_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)
{d e : ℕ}
{x y z : S.ARVertex}
(f : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y))
(g : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) e y z))
(f' : S.label x ⟶ S.label y)
(hf' : f' ∈ S.radPow d (S.label x) (S.label y))
(g' : S.label y ⟶ S.label z)
(hg' : g' ∈ S.radPow e (S.label y) (S.label z))
(hf : (S.phi b d x y) f = S.layerClass f' hf')
(hg : (S.phi b e y z) g = S.layerClass g' hg')
:
∃ (hfg : CategoryTheory.CategoryStruct.comp ↑f ↑g ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) (d + e) x z)
(hfg' : CategoryTheory.CategoryStruct.comp f' g' ∈ S.radPow (d + e) (S.label x) (S.label z)),
(S.phi b (d + e) x z) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, hfg⟩ = S.layerClass (CategoryTheory.CategoryStruct.comp f' g') hfg'
theorem
MultiplicativeBasisDeformations.IndSkeleton.gradedRealization_full
{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), DirectSum.IsInternal fun (d : ℕ) => ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) ∧ ∃ (φ :
(d : ℕ) →
(x y : S.ARVertex) →
↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) ≃ₗ[k] S.layer d (S.label x) (S.label y)),
(∀ (x y : S.ARVertex) (a : x ⟶ y)
(ha :
ScalarMeshCategory.arrowMor (S.arCoefficients b) a ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) 1 x y),
(φ 1 x y) ⟨ScalarMeshCategory.arrowMor (S.arCoefficients b) a, ha⟩ = (b x y) a) ∧ ∀ (d e : ℕ) (x y z : S.ARVertex) (f : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y))
(g : ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) e y z)) (f' : S.label x ⟶ S.label y)
(hf' : f' ∈ S.radPow d (S.label x) (S.label y)) (g' : S.label y ⟶ S.label z)
(hg' : g' ∈ S.radPow e (S.label y) (S.label z)),
(φ d x y) f = S.layerClass f' hf' →
(φ e y z) g = S.layerClass g' hg' →
∃ (hfg :
CategoryTheory.CategoryStruct.comp ↑f ↑g ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) (d + e) x z)
(hfg' : CategoryTheory.CategoryStruct.comp f' g' ∈ S.radPow (d + e) (S.label x) (S.label z)),
(φ (d + e) x z) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, hfg⟩ = S.layerClass (CategoryTheory.CategoryStruct.comp f' g') hfg'
Proposition 2.6(3) (prop:graded-realization).