Lemma 2.1: normed bases from the basic algebra #
lem:nonbasic-basis (graded-category.tex). Let B₀ = eAe with
AeA = A have a normed multiplicative basis with primitive idempotents e_i.
"Every basis element b belongs to one corner: in b = Σ e_i b e_j, each nonzero
summand is a basis element by multiplicativity […]." Each primitive idempotent
f of a complete set of A has fA ≅ e_i A, given by elements u ∈ fAe_i,
v ∈ e_iAf with uv = f, vu = e_i (here from 1 ∈ AeA and the local corner
fAf). "For each element b ∈ e_iB₀e_j of the given basis, take all its
single-entry matrices E_{iα,jβ}(b)": here u_s b v_t. "Their multiplication is
E_{iα,jβ}(b) E_{lγ,mδ}(c) = E_{iα,mδ}(bc) if (j,β) = (l,γ), 0 otherwise
[…]. The single-entry matrices E_{iα,iα}(e_i) form a complete set of primitive
orthogonal idempotents. The radical powers of A have the same block
description with e_i (rad B₀)^n e_j in each block."
structure
MultiplicativeBasisDeformations.Nonbasic.Hyp
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
(he : IsIdempotentElem e)
{ι : Type v}
(b : Module.Basis ι k he.Corner)
(E : Finset ι)
:
The hypotheses on the basis of B₀ = eAe.
- ortho : CompleteOrthogonalIdempotents fun (i : ↥E) => b ↑i
- mul : IsMultiplicativeBasis b
- prim (i : ι) : i ∈ E → IsPrimitiveIdempotent (b i)
- rad (n : ℕ) : 1 ≤ n → Submodule.span k (⇑b '' {i : ι | b i ∈ algebraRadicalPow k he.Corner n}) = algebraRadicalPow k he.Corner n
Instances For
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.bv
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
(he : IsIdempotentElem e)
{ι : Type v}
(b : Module.Basis ι k he.Corner)
(l : ι)
:
A
A basis element of B₀, in A.
Instances For
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.ε
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
{ι : Type v}
{E : Finset ι}
(he : IsIdempotentElem e)
(b : Module.Basis ι k he.Corner)
(i : ↥E)
:
A
The idempotent e_i of B₀, in A.
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.ε_orth
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
{i j : ↥E}
(hij : i ≠ j)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.triple
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(i l j : ι)
:
b i * b l * b j = 0 ∨ ∃ (m : ι), b i * b l * b j = b m
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.exists_corner
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
Every basis element lies in one corner e_i B₀ e_j.
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Hyp.src
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
↥E
The source idempotent of a basis element.
Instances For
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Hyp.tgt
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
↥E
The target idempotent of a basis element.
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.src_tgt
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.src_mul
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.mul_tgt
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(l : ι)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.ε_mul_bv
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(i : ↥E)
(l : ι)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.bv_mul_ε
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(i : ↥E)
(l : ι)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.ε_primitive
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(i : ↥E)
:
IsPrimitiveIdempotent (ε he b i)
e_i is primitive in A.
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.exists_sum_of_mem_span
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e a : A}
(ha : a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
:
∃ (m : ℕ) (p : Fin m → A) (q : Fin m → A), ∑ r : Fin m, p r * e * q r = a
An element of the two-sided ideal AeA is a sum Σ p_r e q_r.
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.exists_match
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(hfull : 1 ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
{f0 : A}
(hp : IsPrimitiveIdempotent f0)
:
Each primitive idempotent f of A is isomorphic to some e_i: there are
u ∈ fAe_i, v ∈ e_iAf with uv = f and vu = e_i. Write
f = Σ f p_r e_i q_r f from 1 ∈ AeA; the corner fAf is local, so one summand is
a unit.
structure
MultiplicativeBasisDeformations.Nonbasic.Match
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
:
Type v
The matching data: a complete set f_s of primitive orthogonal idempotents of
A, with f_s A ≅ e_{σ s} A given by u_s, v_s.
- n : ℕ
- f : Fin self.n → A
- hf : CompleteOrthogonalIdempotents self.f
- prim (s : Fin self.n) : IsPrimitiveIdempotent (self.f s)
- σ : Fin self.n → ↥E
- u : Fin self.n → A
- v : Fin self.n → A
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Hyp.nonempty_match
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
(H : Hyp he b E)
(hfull : 1 ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
:
Nonempty (Match H)
def
MultiplicativeBasisDeformations.Nonbasic.P
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
(he : IsIdempotentElem e)
:
A →ₗ[k] he.Corner
The corner projection a ↦ eae.
Instances For
def
MultiplicativeBasisDeformations.Nonbasic.Match.Idx
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
Type v
The index set: triples (s, l, t) with b_l ∈ e_{σ s} B₀ e_{σ t}.
Instances For
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Match.Eb
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(x : M.Idx)
:
A
The basis element E_{s,t}(b_l) = u_s b_l v_t.
Instances For
def
MultiplicativeBasisDeformations.Nonbasic.Match.T
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(s t : Fin M.n)
:
he.Corner →ₗ[k] A
x ↦ u_s x v_t on B₀.
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.T_apply
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(s t : Fin M.n)
(x : he.Corner)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.v_Eb_u
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(y : M.Idx)
(s t : Fin M.n)
:
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Match.κ
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(y : M.Idx)
:
A →ₗ[k] k
The coordinate of index y: a ↦ (coefficient of b_l in v_s a u_t).
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.linearIndependent_Eb
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
LinearIndependent k M.Eb
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.T_mem_span
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(s t : Fin M.n)
(S : Set ι)
(Q : Submodule k A)
(hQ : ∀ (y : M.Idx), (↑y).2.1 ∈ S → M.Eb y ∈ Q)
{z : he.Corner}
(hz : z ∈ Submodule.span k (⇑b '' S))
:
(M.T s t) z ∈ Q
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.span_Eb
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
⊤ ≤ Submodule.span k (Set.range M.Eb)
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Match.basis
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
Module.Basis M.Idx k A
The basis E_{s,t}(b_l) of A.
Instances For
def
MultiplicativeBasisDeformations.Nonbasic.Match.Fidx
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(s : Fin M.n)
:
M.Idx
The index of E_{s,s}(e_{σ s}) = f_s.
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.Fidx_injective
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
Function.Injective M.Fidx
noncomputable def
MultiplicativeBasisDeformations.Nonbasic.Match.Fset
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
:
Finset M.Idx
The idempotent indices.
Instances For
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.basis_of_mem_Fset
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
{i : M.Idx}
(hi : i ∈ M.Fset)
:
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.Eb_mem_radPow
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
{n : ℕ}
(hn : 1 ≤ n)
(y : M.Idx)
(hy : b (↑y).2.1 ∈ algebraRadicalPow k he.Corner n)
:
M.Eb y ∈ algebraRadicalPow k A n
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.basis_radicalPow
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(hfull : 1 ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
(n : ℕ)
(hn : 1 ≤ n)
:
Submodule.span k (⇑M.basis '' {i : M.Idx | M.basis i ∈ algebraRadicalPow k A n}) = algebraRadicalPow k A n
theorem
MultiplicativeBasisDeformations.Nonbasic.Match.hasNormedBasis
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
{he : IsIdempotentElem e}
{ι : Type v}
{b : Module.Basis ι k he.Corner}
{E : Finset ι}
{H : Hyp he b E}
(M : Match H)
(hfull : 1 ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
:
Lemma 2.1.