Proposition 7.9 on A₀ for an arbitrary family #
prop:family-criterion (characteristic-two-construction.tex): let I₀ index the nonzero
spaces HH²(A₀)_{χ_i} of Proposition 6.1, and let normalized S-relative two-cochains μ_i,
i ∈ I₀, satisfy (1) each μ_i is homogeneous of character χ_i with nonzero class, (2) the
family product m + Σ t_i μ_i is associative, (3) every binary fibre has the basis of kP as a
normed multiplicative basis, and every scalar fibre has ray category P. Then a binary fibre is isomorphic to A, the
transported basis is a normed multiplicative ray basis, and the isomorphism preserves each initial
ray line up to a nonzero scalar.
Here the rows and characters are those of Proposition 6.1 with their dual mesh weights
(rowChar), I₀ is the set of rows with a nonzero class in positive internal degree
(HH2Nonzero, I0), and A is any positive filtered deformation B of A₀
(familyCriterion_A0). The internal degree of μ_i is not assumed: it is the length coordinate
of χ_i (RaySys.Sys.hasDeg₂_of_char). Associativity is required at every scalar parameter,
which follows from associativity over the polynomial ring. Hypothesis (3) is stated on the
fibre algebra itself (Fib (fibAM …)), and used for binary fibres; it is transported to B
along the isomorphism (IsNormedMultiplicativeBasis.map_algEquiv, IsRayPres.map).
theorem
MultiplicativeBasisDeformations.RaySys.Sys.hasDeg₂_of_char
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
(S : Sys V R L)
(k : Type u)
[Field k]
[IsAlgClosed k]
{Λ : Type u}
[Ring Λ]
[Algebra k Λ]
(Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ)
{G : LenGrading k Λ}
{W : LatGrading k Λ L}
(hG : ∀ (r : R), G.IsHom (S.P.deg (S.P.wt r)).toNat (Θ (S.P.b k r)))
(hW : ∀ (r : R), W.IsHom (S.P.wt r) (Θ (S.P.b k r)))
{χ : L}
(hχ : 0 ≤ S.P.deg χ)
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hc : W.Char₂ χ φ)
:
A cochain of character χ has internal degree deg χ.
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.MeshWalk.rowChar
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{ι : Type}
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(i : ι)
:
DLat ι
The character χ_i of a row of Proposition 6.1.
Instances For
def
MultiplicativeBasisDeformations.MeshWalk.HH2Nonzero
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(i : ι)
:
A row with a nonzero space HH²(A₀)_{χ_i} in positive internal degree.
Instances For
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.MeshWalk.I0
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
:
The index set I₀.
Instances For
@[instance_reducible]
noncomputable instance
MultiplicativeBasisDeformations.MeshWalk.instFintypeI0
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
:
Fintype (I0 D v₀ hF Wd Rw)
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.famMulI
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{v₀ : V}
{hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ}
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{Wd : ι → MeshWt Q ℤ}
{Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(μ : I0 D v₀ hF Wd Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ)
(lam : I0 D v₀ hF Wd Rw → k)
:
(CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ
The family product m + Σ λ_i μ_i.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.famMulI_apply
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(μ : I0 D v₀ hF Wd Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ)
(lam : I0 D v₀ hF Wd Rw → k)
(a b : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.mLam_reindex
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
{n : ℕ}
(e : Fin n ≃ I0 D v₀ hF Wd Rw)
(μ : I0 D v₀ hF Wd Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ)
(lam : Fin n → k)
(a b : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
((LenGrading.mLam (fun (j : Fin n) => μ (e j)) lam) a) b = ((famMulI μ fun (i : I0 D v₀ hF Wd Rw) => lam (e.symm i)) a) b
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.fibAM
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{v₀ : V}
{hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ}
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{Wd : ι → MeshWt Q ℤ}
{Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
{μ : I0 D v₀ hF Wd Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hrel : ∀ (i : I0 D v₀ hF Wd Rw), LenGrading.IsRel₂ (VxA0 D v₀ hF Wd) (μ i))
(hassoc :
∀ (lam : I0 D v₀ hF Wd Rw → k) (a b z : (CatAlg.Alg D.F0)ᵐᵒᵖ),
((famMulI μ lam) (((famMulI μ lam) a) b)) z = ((famMulI μ lam) a) (((famMulI μ lam) b) z))
(lam : I0 D v₀ hF Wd Rw → k)
:
AssocMul k (CatAlg.Alg D.F0)ᵐᵒᵖ
A binary or scalar fibre: the family product at lam as an associative unital product.
Instances For
def
MultiplicativeBasisDeformations.PrimitiveIdempotents.mapEquiv
{k : Type u}
[Field k]
{B B' : Type u}
[Ring B]
[Algebra k B]
[Ring B']
[Algebra k B']
(F : PrimitiveIdempotents B)
(ψ : B ≃ₐ[k] B')
:
The image of a complete set of primitive idempotents under an algebra isomorphism.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.familyCriterion_A0
{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}
{L : CatAlg.LocalFamily (meshFam Q c)}
(D : CatAlg.MeshData (meshFam Q c) L)
[IsAlgClosed k]
[hone : ∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(v₀ : V)
(hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWt Q ℤ)
(Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(J : D.InjData)
(h1 : DegOne D)
[Fintype ↑Q.nonprojective]
(hWd : ∀ (i j : ι), rowWt (Wd i) (Rw j) = if j = i then 1 else 0)
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
(μ : I0 D v₀ hF Wd Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ)
(hrel : ∀ (i : I0 D v₀ hF Wd Rw), LenGrading.IsRel₂ (VxA0 D v₀ hF Wd) (μ i))
(hchar : ∀ (i : I0 D v₀ hF Wd Rw), (latA0 (dualWt Wd) ⋯ D).Char₂ (rowChar Wd Rw ↑i) (μ i))
(hcoc : ∀ (i : I0 D v₀ hF Wd Rw), LenGrading.IsCocycle₂ (μ i))
(hnz : ∀ (i : I0 D v₀ hF Wd Rw), ¬∃ (f : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), μ i = LenGrading.cobdry k f)
(hassoc :
∀ (lam : I0 D v₀ hF Wd Rw → k) (a b z : (CatAlg.Alg D.F0)ᵐᵒᵖ),
((famMulI μ lam) (((famMulI μ lam) a) b)) z = ((famMulI μ lam) a) (((famMulI μ lam) b) z))
(hfib :
∀ (lam : I0 D v₀ hF Wd Rw → k),
(∀ (i : I0 D v₀ hF Wd Rw), lam i = 0 ∨ lam i = 1) →
IsNormedMultiplicativeBasis ((basisR D v₀ hF).map (Fib.toΛ (fibAM hrel hassoc lam)).symm) ∧ ∃ (F : PrimitiveIdempotents (Fib (fibAM hrel hassoc lam))) (ιF : D.PV ≃ Fin F.m),
F.IsRayPres (A0Mult D v₀ hF) ιF fun (r : RayA0 D v₀) =>
(Fib.toΛ (fibAM hrel hassoc lam)).symm ((basisR D v₀ hF) r))
{B : Type u}
[Ring B]
[Algebra k B]
[FiniteDimensional k B]
(Pf : PosFiltration (lenA0 D ⋯) B)
:
∃ (lam : I0 D v₀ hF Wd Rw → k) (_ : ∀ (i : I0 D v₀ hF Wd Rw), lam i = 0 ∨ lam i = 1) (Ψ : (CatAlg.Alg D.F0)ᵐᵒᵖ ≃ₗ[k] B),
(∀ (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), Ψ (((famMulI μ lam) a) b) = Ψ a * Ψ b) ∧ IsNormedMultiplicativeBasis ((basisR D v₀ hF).map Ψ) ∧ (∃ (F : PrimitiveIdempotents B) (ιF : D.PV ≃ Fin F.m),
F.IsRayPres (A0Mult D v₀ hF) ιF fun (r : RayA0 D v₀) => Ψ ((basisR D v₀ hF) r)) ∧ ∀ (r : RayA0 D v₀),
∃ (t : k),
t ≠ 0 ∧ (Pf.σ ((SysD D v₀ hF Wd).P.deg ((SysD D v₀ hF Wd).P.wt r)).toNat) (Ψ ((basisR D v₀ hF) r)) = t • (basisR D v₀ hF) r
Proposition 7.9 on A₀ (prop:family-criterion): for the rows and characters of
Proposition 6.1 and any family μ_i, i ∈ I₀, of normalized S-relative cocycles of character
χ_i with nonzero classes, whose family product is associative and whose binary fibres have the
basis of kP as a normed multiplicative basis with ray category P: every positive filtered
deformation B of A₀ is isomorphic to a binary fibre; the transported basis is a normed
multiplicative ray basis of B presenting P, and the leading term of the image of each ray
vector b_r is a nonzero multiple of b_r.