The retained coefficients are nonzero (Proposition 12.8, a_i ∈ k^*) #
deformation-refinements.tex: "Specializing t_j = ε, all other parameters zero and
ε² = 0, identifies a_j[p_j] with Ψ[μ_j]. This is nonzero because Ψ is injective
(Proposition 7.6). Hence a_j ≠ 0."
At t = 1 the lifts have relative weights in the cone C of the χ_i, and χ_j is an atom of
C. The components of relative weight χ_j (and internal degree q_j) of the lifted actions
and arrows are therefore the square-zero lifts of Lemma 6.6 for μ_j (ν1, y1), i.e. the
specialization t = ε e_j; their mesh errors are λ_j R_j (zE_psi). So Ψ[μ_j] = λ_j [R_j],
and λ_j ≠ 0 because μ_j is not a coboundary.
The cocycle condition #
theorem
MultiplicativeBasisDeformations.MeshWalk.famMul_single
{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}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
(j : I)
(s : k)
(a b : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
((famMul D μ (Pi.single j s)) a) b = a * b + s • ((μ j) a) b
theorem
MultiplicativeBasisDeformations.MeshWalk.famHyp_cocycle
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
(H : FamHyp D hfin μ qd)
[Infinite k]
(j : I)
:
GExt.IsHCocycle (μ j)
Each μ_j is a Hochschild cocycle: the linear term of associativity in t_j.
The atoms of the cone #
theorem
MultiplicativeBasisDeformations.MeshWalk.χ_injective
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
:
Function.Injective χ
theorem
MultiplicativeBasisDeformations.MeshWalk.χ_atom
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
(j : I)
(u : Wt)
:
χ_j is an atom of the cone.
theorem
MultiplicativeBasisDeformations.MeshWalk.eq_of_χ_sub_mem
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
{i j : I}
(h : χ j - χ i ∈ cone χ)
:
i = j
The χ_j-parts of the lifted actions #
theorem
MultiplicativeBasisDeformations.MeshWalk.sum_antidiag_fst
{X : Type u_1}
[AddCommMonoid X]
(n : ℕ)
(f : ℕ × ℕ → X)
:
(∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, if x.1 = 0 then f x else 0) = f (0, n)
theorem
MultiplicativeBasisDeformations.MeshWalk.sum_antidiag_snd
{X : Type u_1}
[AddCommMonoid X]
(n : ℕ)
(f : ℕ × ℕ → X)
:
(∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, if x.2 = 0 then f x else 0) = f (n, 0)
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.ν1
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
(H : FamHyp D hfin μ qd)
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i))
(J : D.InjData)
(h1 : DegOne D)
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
(j : I)
(X : V)
:
CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)
The first-order action ν = (ν_{q_j})_{χ_j}, the t_j-linear part of the lifted action.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.ν1_hom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
{β α : Wt}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (grEv W hfin D X).IsHom β m)
(ha : (grA0 W hfin D).IsHom α a)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.act_isHom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
[Infinite k]
(X : V)
{β α : Wt}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (grEv W hfin D X).IsHom β m)
(ha : (grA0 W hfin D).IsHom α a)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.proj_νν
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
(l j' : ℕ)
{β α α' : Wt}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a b : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (grEv W hfin D X).IsHom β m)
(ha : (grA0 W hfin D).IsHom α a)
(hb : (grA0 W hfin D).IsHom α' b)
:
((grEv W hfin D X).proj (β + α + α' + χ j))
((((act1 H W hχ J h1 hco X).ν l) ((((act1 H W hχ J h1 hco X).ν j') m) a)) b) = (if j' = 0 then
((grEv W hfin D X).proj (β + α + α' + χ j)) ((((act1 H W hχ J h1 hco X).ν l) (((gmodEv D hfin X).act m) a)) b)
else 0) + if l = 0 then
((gmodEv D hfin X).act (((grEv W hfin D X).proj (β + α + χ j)) ((((act1 H W hχ J h1 hco X).ν j') m) a))) b
else 0
The atom component of ν_l(ν_{j'}(m, a), b).
theorem
MultiplicativeBasisDeformations.MeshWalk.P1μ_eq
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
[Infinite k]
(l : ℕ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.P1μ_bottom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i))
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
[Infinite k]
(l : ℕ)
{α α' : Wt}
{a b : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(ha : (grA0 W hfin D).IsHom α a)
(hb : (grA0 W hfin D).IsHom α' b)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.P1μ_atom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
(hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i))
(hco : ∀ (i : I), coords (χ i) = Pi.single i 1)
[Infinite k]
(j : I)
(l : ℕ)
{α α' : Wt}
{a b : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(ha : (grA0 W hfin D).IsHom α a)
(hb : (grA0 W hfin D).IsHom α' b)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.proj_νμ
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
(l j' : ℕ)
{β α α' : Wt}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a b : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (grEv W hfin D X).IsHom β m)
(ha : (grA0 W hfin D).IsHom α a)
(hb : (grA0 W hfin D).IsHom α' b)
:
((grEv W hfin D X).proj (β + α + α' + χ j))
((((act1 H W hχ J h1 hco X).ν j') m) (((((famSplit H 1).posDef ⋯).μ l) a) b)) = (if l = 0 then ((grEv W hfin D X).proj (β + α + α' + χ j)) ((((act1 H W hχ J h1 hco X).ν j') m) (a * b)) else 0) + if j' = 0 then ((gmodEv D hfin X).act m) (if qd j = l then ((μ j) a) b else 0) else 0
The atom component of ν_{j'}(m, μ_l(a, b)).
theorem
MultiplicativeBasisDeformations.MeshWalk.ν1_eq
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
(m : CatAlg.Rep D.F0 (meshFam Q c X))
(a b : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
The first-order action satisfies the square-zero equation for μ_j.
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.L1
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
:
GExt.ActLift (μ j) (↑(qd j)) (gmodEv D hfin X)
The first-order lifted action as a square-zero lift for μ_j.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.L1_act
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(j : I)
(X : V)
(m : CatAlg.Rep D.F0 (meshFam Q c X))
(a : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
Joint homogeneity #
theorem
MultiplicativeBasisDeformations.MeshWalk.a0Proj_zproj
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
(γ : Wt)
(d : ℤ)
(v : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.zproj_wHom_ev
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
[Infinite k]
{X : V}
{β : Wt}
{v : CatAlg.Rep D.F0 (meshFam Q c X)}
(hv : (grEv W hfin D X).IsHom β v)
(p : ℤ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.zproj_wHom_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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{α : Wt}
{v : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hv : (grA0 W hfin D).IsHom α v)
(p : ℤ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.wz_ext_lin
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
[Infinite k]
{y x : V}
{f g : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(h :
∀ (β : Wt) (p : ℤ) (v : CatAlg.Rep D.F0 (meshFam Q c y)),
(grEv W hfin D y).IsHom β v → (zgrEv D hfin y).IsHom p v → f v = g v)
:
f = g
Linear maps agreeing on jointly homogeneous vectors agree.
theorem
MultiplicativeBasisDeformations.MeshWalk.wz_ext_bil
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
[Infinite k]
{y x : V}
{f g : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(h :
∀ (β : Wt) (p : ℤ) (α : Wt) (d : ℤ) (v : CatAlg.Rep D.F0 (meshFam Q c y)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ),
(grEv W hfin D y).IsHom β v →
(zgrEv D hfin y).IsHom p v → (grA0 W hfin D).IsHom α a → (galgA0 D hfin).gr.IsHom d a → (f v) a = (g v) a)
:
f = g
Bilinear maps agreeing on jointly homogeneous pairs agree.
theorem
MultiplicativeBasisDeformations.MeshWalk.zproj_shift
{k : Type u}
[Field k]
{Y : Type u_1}
{Z : Type u_2}
[AddCommGroup Y]
[Module k Y]
[AddCommGroup Z]
[Module k Z]
{gY : GExt.ZGr Y}
{gZ : GExt.ZGr Z}
{s : ℤ}
{u : Y →ₗ[k] Z}
(hu : ∀ (e : ℤ) (v : Y), gY.IsHom e v → gZ.IsHom (e + s) (u v))
(e : ℤ)
(v : Y)
:
A map raising the degree by exactly s commutes with the degree projections.
The total lifted action: bottom part and degree components #
theorem
MultiplicativeBasisDeformations.MeshWalk.tot_bottom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(X : V)
{β α : Wt}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (grEv W hfin D X).IsHom β m)
(ha : (grA0 W hfin D).IsHom α a)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.tot_wz
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(X : V)
(δ : Wt)
{p d : ℤ}
{m : CatAlg.Rep D.F0 (meshFam Q c X)}
{a : (CatAlg.Alg D.F0)ᵐᵒᵖ}
(hm : (zgrEv D hfin X).IsHom p m)
(ha : (galgA0 D hfin).gr.IsHom d a)
(n : ℕ)
:
The first-order parts of the lifted arrows #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.y1
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(j : I)
{y x : V}
(a : y ⟶ x)
:
CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)
The first-order arrow g_a: the part of relative weight χ_j and internal degree
1 + q_j of the lifted arrow.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.y1_hom
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(j : I)
{y x : V}
(a : y ⟶ x)
{β : Wt}
{p : ℤ}
{v : CatAlg.Rep D.F0 (meshFam Q c y)}
(hv : (grEv W hfin D y).IsHom β v)
(hp : (zgrEv D hfin y).IsHom p v)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.y1_lift
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(j : I)
{y x : V}
(a : y ⟶ x)
(m : CatAlg.Rep D.F0 (meshFam Q c y))
(b : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
The first-order arrows satisfy the square-zero linearity of Lemma 6.6.
The lift data for μ_j and its mesh errors #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.LdPsi
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(j : I)
:
LiftData D hfin (qd j) (μ j)
The first-order lift data for μ_j: the specialization t = ε e_j of the lifts.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.zE_psi
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2)
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(hA : ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0)
(j : I)
(x : ↑Q.nonprojective)
:
zE (LdPsi A j) x = lam j • rs D (ScalarMeshCategory.row c (Rw j).fst (Rw j).snd x)
The mesh errors of the first-order lift data are λ_j R_j.
theorem
MultiplicativeBasisDeformations.MeshWalk.Ψc_psi
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2)
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(hA : ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0)
(j : I)
:
Ψc (LdPsi A j) = lam j • Submodule.Quotient.mk (ScalarMeshCategory.row c (Rw j).fst (Rw j).snd)
Ψ[μ_j] = λ_j [R_j].
theorem
MultiplicativeBasisDeformations.MeshWalk.lam_ne_zero
{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}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2)
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(hA : ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0)
(j : I)
(hnc :
¬∃ (Hc : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ),
(∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ),
(galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑(qd j)) (Hc a)) ∧ μ j = GExt.hcobdry Hc)
:
lam j ≠ 0
The retained coefficients are nonzero (a_j ∈ k^*), when μ_j is not a coboundary.