A first-order functor on the projective corner trivializes the deformation #
integral-deformations.tex (proof of Lemma 10.2): "If its value is zero, arrow changes
remove all first-order mesh errors. The Hom category of the lifted modules becomes constant.
Restricting to its actual projective corner trivializes the algebra deformation."
Ring-generic form. Modules N_X over an R-algebra Λ carry first-order lifts of their
actions for a cocycle μ; the arrows φ_a and their corrections g_a satisfy the mesh
relations exactly and to first order. At projective labels p the module is regular,
N_p ≅ e_pΛ with generator w_p and inverse ψ_p, its lifted action is the regular one, and
evaluation at w_p identifies RQ(p, s) modulo the mesh ideal with N_p e_s. Then μ is a
Hochschild coboundary (eq_hcobdry), through the derivation Δ(b) = ∑_p ψ_p Δ_p(w_p b) with
Δ_p(n) = ∑_s δ(n e_s)(w_s).
structure
MultiplicativeBasisDeformations.CornerDeriv.Hyp
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(u : MeshCoefficients R Q)
(N : V → Type v)
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
(MM : (X : V) → GExt.GMod GΛ (N X))
(Lf : (X : V) → GExt.ActLift μ q (MM X))
(φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x)
{P : Type}
[Fintype P]
(lab : P → V)
(e : P → Λ)
(w : (p : P) → N (lab p))
(ψ : (p : P) → N (lab p) →ₗ[R] Λ)
:
The hypotheses of the projective corner argument.
- e_idem (p : P) : e p * e p = e p
- e_sum : ∑ p : P, e p = 1
- mesh (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • φ a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd) = 0
- zmesh (x : ↑Q.nonprojective) : ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • (φ a.snd ∘ₗ g ((Q.mate x a.fst) a.snd) + g a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd)) = 0
- w_e (p : P) : ((MM (lab p)).act (w p)) (e p) = w p
- surj (s p : P) (n : N (lab p)) : ((MM (lab p)).act n) (e s) = n → ∃ (F : LinearPaths.obj (lab s) ⟶ LinearPaths.obj (lab p)), ((PathEval.evL N fun {y x : V} => φ) F) (w s) = n
- inj (s p : P) (F : LinearPaths.obj (lab s) ⟶ LinearPaths.obj (lab p)) : ((PathEval.evL N fun {y x : V} => φ) F) (w s) = 0 → F ∈ (CategoricalIdeal.HomIdeal.linearSpan R (meshRelations u)).hom (LinearPaths.obj (lab s)) (LinearPaths.obj (lab p))
Instances For
theorem
MultiplicativeBasisDeformations.CornerDeriv.evP_act
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{Y X : V}
(p : Quiver.Path Y X)
(m : N Y)
(b : Λ)
:
(PathEval.evP N (fun {y x : V} => φ) p) (((MM Y).act m) b) = ((MM X).act ((PathEval.evP N (fun {y x : V} => φ) p) m)) b
theorem
MultiplicativeBasisDeformations.CornerDeriv.evL_act
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{Y X : V}
(F : LinearPaths.obj Y ⟶ LinearPaths.obj X)
(m : N Y)
(b : Λ)
:
((PathEval.evL N fun {y x : V} => φ) F) (((MM Y).act m) b) = ((MM X).act (((PathEval.evL N fun {y x : V} => φ) F) m)) b
theorem
MultiplicativeBasisDeformations.CornerDeriv.act_sum_e
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{Y : V}
(m : N Y)
:
∑ s : P, ((MM Y).act m) (e s) = m
theorem
MultiplicativeBasisDeformations.CornerDeriv.ψ_eq_e_mul
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(p : P)
(n : N (lab p))
:
e p * (ψ p) n = (ψ p) n
theorem
MultiplicativeBasisDeformations.CornerDeriv.ψ_act
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(p : P)
(n : N (lab p))
(b : Λ)
:
(ψ p) (((MM (lab p)).act n) b) = (ψ p) n * b
theorem
MultiplicativeBasisDeformations.CornerDeriv.act_e_idem
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{Y : V}
(m : N Y)
(s : P)
:
The derivation on the regular modules #
noncomputable def
MultiplicativeBasisDeformations.CornerDeriv.pre
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(s p : P)
(n : N (lab p))
:
LinearPaths.obj (lab s) ⟶ LinearPaths.obj (lab p)
A preimage of n e_s in RQ(s, p).
Instances For
theorem
MultiplicativeBasisDeformations.CornerDeriv.evL_pre
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(s p : P)
(n : N (lab p))
:
((PathEval.evL N fun {y x : V} => φ) (pre H s p n)) (w s) = ((MM (lab p)).act n) (e s)
theorem
MultiplicativeBasisDeformations.CornerDeriv.δL_eq_pre
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{s p : P}
{n : N (lab p)}
{F : LinearPaths.obj (lab s) ⟶ LinearPaths.obj (lab p)}
(hF : ((PathEval.evL N fun {y x : V} => φ) F) (w s) = ((MM (lab p)).act n) (e s))
:
((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) F) (w s) = ((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) (pre H s p n)) (w s)
noncomputable def
MultiplicativeBasisDeformations.CornerDeriv.Δm
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(p : P)
:
N (lab p) →ₗ[R] N (lab p)
Δ_p(n) = ∑_s δ(n e_s)(w_s).
Instances For
theorem
MultiplicativeBasisDeformations.CornerDeriv.Δm_apply
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(p : P)
(n : N (lab p))
:
(Δm H p) n = ∑ s : P, ((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) (pre H s p n)) (w s)
theorem
MultiplicativeBasisDeformations.CornerDeriv.δL_comm
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{r p : P}
(F : LinearPaths.obj (lab r) ⟶ LinearPaths.obj (lab p))
(n : N (lab r))
:
((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) F) n = (Δm H p) (((PathEval.evL N fun {y x : V} => φ) F) n) - ((PathEval.evL N fun {y x : V} => φ) F) ((Δm H r) n)
δF is the commutator of Δ with F.
theorem
MultiplicativeBasisDeformations.CornerDeriv.Δm_evL
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
{r p : P}
(F : LinearPaths.obj (lab r) ⟶ LinearPaths.obj (lab p))
(n : N (lab r))
:
(Δm H p) (((PathEval.evL N fun {y x : V} => φ) F) n) = ((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) F) n + ((PathEval.evL N fun {y x : V} => φ) F) ((Δm H r) n)
The derivation on Λ #
noncomputable def
MultiplicativeBasisDeformations.CornerDeriv.Δ
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
:
Λ →ₗ[R] Λ
The derivation on Λ: Δ(b) = ∑_p ψ_p(Δ_p(w_p b)).
Instances For
theorem
MultiplicativeBasisDeformations.CornerDeriv.Δ_apply
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(b : Λ)
:
noncomputable def
MultiplicativeBasisDeformations.CornerDeriv.Fpr
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x : Λ)
(p r : P)
:
LinearPaths.obj (lab r) ⟶ LinearPaths.obj (lab p)
The component e_p x e_r of x as a morphism r → p.
Instances For
theorem
MultiplicativeBasisDeformations.CornerDeriv.evL_Fpr
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x : Λ)
(p r : P)
:
((PathEval.evL N fun {y x : V} => φ) (Fpr H x p r)) (w r) = ((MM (lab p)).act (w p)) (x * e r)
theorem
MultiplicativeBasisDeformations.CornerDeriv.evL_Fpr_act
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x : Λ)
(p r : P)
(c : Λ)
:
((PathEval.evL N fun {y x : V} => φ) (Fpr H x p r)) (((MM (lab r)).act (w r)) c) = ((MM (lab p)).act (w p)) (x * e r * c)
theorem
MultiplicativeBasisDeformations.CornerDeriv.ψ_evL_Fpr
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x : Λ)
(p r : P)
(n : N (lab r))
:
(ψ p) (((PathEval.evL N fun {y x : V} => φ) (Fpr H x p r)) n) = e p * x * e r * (ψ r) n
theorem
MultiplicativeBasisDeformations.CornerDeriv.sum_ψ_evL_Fpr
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x : Λ)
(r : P)
(n : N (lab r))
:
∑ p : P, (ψ p) (((PathEval.evL N fun {y x : V} => φ) (Fpr H x p r)) n) = x * (ψ r) n
theorem
MultiplicativeBasisDeformations.CornerDeriv.act_w_mul
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x b : Λ)
(p : P)
:
((MM (lab p)).act (w p)) (x * b) = ∑ r : P, ((PathEval.evL N fun {y x : V} => φ) (Fpr H x p r)) (((MM (lab r)).act (w r)) b)
theorem
MultiplicativeBasisDeformations.CornerDeriv.Δ_mul_sub
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x b : Λ)
:
(Δ H) (x * b) - x * (Δ H) b = ∑ p : P,
∑ r : P,
(ψ p) (((PathEval.δL N (fun {y x : V} => φ) fun {y x : V} => g) (Fpr H x p r)) (((MM (lab r)).act (w r)) b))
theorem
MultiplicativeBasisDeformations.CornerDeriv.ψ_w_one
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(r : P)
:
(ψ r) (w r) = e r
theorem
MultiplicativeBasisDeformations.CornerDeriv.Δ_eq
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(x b : Λ)
:
The derivation identity, the hypothesis of GExt.eq_hcobdry_of_derivation.
theorem
MultiplicativeBasisDeformations.CornerDeriv.eq_hcobdry
{R : Type u}
[CommRing R]
{Λ : Type u_1}
[Ring Λ]
[Algebra R Λ]
{GΛ : GExt.GAlg Λ}
{μ : Λ →ₗ[R] Λ →ₗ[R] Λ}
{q : ℤ}
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients R Q}
{N : V → Type v}
[(X : V) → AddCommGroup (N X)]
[(X : V) → Module R (N X)]
{MM : (X : V) → GExt.GMod GΛ (N X)}
{Lf : (X : V) → GExt.ActLift μ q (MM X)}
{φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x}
{P : Type}
[Fintype P]
{lab : P → V}
{e : P → Λ}
{w : (p : P) → N (lab p)}
{ψ : (p : P) → N (lab p) →ₗ[R] Λ}
(H : Hyp u N MM Lf (fun {y x : V} => φ) (fun {y x : V} => g) lab e w ψ)
(hμ : GExt.IsHCocycle μ)
:
∃ (h : Λ →ₗ[R] Λ), μ = GExt.hcobdry h
The trivialization: μ is a Hochschild coboundary.