Proposition 7.9 for a basic representation-finite algebra #
prop:family-criterion (characteristic-two-construction.tex), for A basic and
representation-finite over an algebraically closed field, A₀ the projective corner of its
Auslander–Reiten mesh category, and the rows and dual weights of Proposition 6.1: for any family
μ_i, i ∈ I₀, satisfying (1)–(3), A is isomorphic to a binary fibre, the transported basis is
a normed multiplicative ray basis of A presenting P = ray A₀, and the leading term of the
image of each ray vector b_r (for the radical filtration of A, posFiltA) is a nonzero
multiple of b_r. The argument does not use the characteristic.
theorem
MultiplicativeBasisDeformations.IndSkeleton.familyCriterion
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{n : ℕ}
{e : Fin n → A}
(he : CompleteOrthogonalIdempotents e)
(hprim : ∀ (i : Fin n), IsPrimitiveIdempotent (e i))
(hbasic :
∀ (i j : Fin n), (∃ (x : A) (y : A), e i * x * e j = x ∧ e j * y * e i = y ∧ x * y = e i ∧ y * x = e j) → i = j)
(v₀ : S.ARVertex)
{ι : Type}
[Fintype ι]
[DecidableEq ι]
(Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ)
(Rw : ι → (x : ↑S.arTranslationQuiver.nonprojective) × Quiver.Path ↑(S.arTranslationQuiver.tau x) ↑x)
:
have hF := ⋯;
(∀ (i j : ι), MeshWalk.rowWt (Wd i) (Rw j) = if j = i then 1 else 0) →
ScalarMeshCategory.CokerSpan (S.arCoefficients b) (Set.range Rw) →
∀
(μ :
MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw →
(CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ),
(∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw),
(MeshWalk.latA0 (MeshWalk.dualWt Wd) ⋯ (S.arMeshData b)).Char₂ (MeshWalk.rowChar Wd Rw ↑i) (μ i)) →
(∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw), LenGrading.IsCocycle₂ (μ i)) →
(∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw),
¬∃ (f : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ),
μ i = LenGrading.cobdry k f) →
∀
(hrel :
∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw),
LenGrading.IsRel₂ (MeshWalk.VxA0 (S.arMeshData b) v₀ hF Wd) (μ i))
(hassoc :
∀ (lam : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw → k) (a b' z : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ),
((MeshWalk.famMulI μ lam) (((MeshWalk.famMulI μ lam) a) b')) z = ((MeshWalk.famMulI μ lam) a) (((MeshWalk.famMulI μ lam) b') z)),
(∀ (lam : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw → k),
(∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw), lam i = 0 ∨ lam i = 1) →
IsNormedMultiplicativeBasis
((MeshWalk.basisR (S.arMeshData b) v₀ hF).map (Fib.toΛ (MeshWalk.fibAM hrel hassoc lam)).symm) ∧ ∃ (F : PrimitiveIdempotents (Fib (MeshWalk.fibAM hrel hassoc lam))) (ιF :
(S.arMeshData b).PV ≃ Fin F.m),
F.IsRayPres (MeshWalk.A0Mult (S.arMeshData b) v₀ hF) ιF
fun (r : MeshWalk.RayA0 (S.arMeshData b) v₀) =>
(Fib.toΛ (MeshWalk.fibAM hrel hassoc lam)).symm
((MeshWalk.basisR (S.arMeshData b) v₀ hF) r)) →
∃ (lam : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw → k) (_ :
∀ (i : MeshWalk.I0 (S.arMeshData b) v₀ hF Wd Rw), lam i = 0 ∨ lam i = 1) (Ψ :
(CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ ≃ₗ[k] A),
(∀ (a b' : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ), Ψ (((MeshWalk.famMulI μ lam) a) b') = Ψ a * Ψ b') ∧ IsNormedMultiplicativeBasis ((MeshWalk.basisR (S.arMeshData b) v₀ hF).map Ψ) ∧ (∃ (F : PrimitiveIdempotents A) (ιF : (S.arMeshData b).PV ≃ Fin F.m),
F.IsRayPres (MeshWalk.A0Mult (S.arMeshData b) v₀ hF) ιF
fun (r : MeshWalk.RayA0 (S.arMeshData b) v₀) =>
Ψ ((MeshWalk.basisR (S.arMeshData b) v₀ hF) r)) ∧ ∀ (r : MeshWalk.RayA0 (S.arMeshData b) v₀),
∃ (t : k),
t ≠ 0 ∧ ((S.posFiltA b he hprim hbasic).σ
((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.deg
((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.wt r)).toNat)
(Ψ ((MeshWalk.basisR (S.arMeshData b) v₀ hF) r)) = t • (MeshWalk.basisR (S.arMeshData b) v₀ hF) r
Proposition 7.9 (prop:family-criterion) for a basic representation-finite algebra A.