The radical of a corner #
For Lemma 2.1 (graded-category.tex): "The radical powers of A have
the same block description with e_i (rad B₀)^n e_j in each block." For an
idempotent e the radical of eAe is e (rad A) e (cornerVal_mem_jacobson,
cornerMk_mem_jacobson); when AeA = A the same holds for all radical powers
(corner_mem_radPow), by inserting 1 ∈ AeA between the factors.
theorem
MultiplicativeBasisDeformations.isUnit_one_sub_of_mem_jacobson
{R : Type u_1}
[Ring R]
[IsDedekindFiniteMonoid R]
{x : R}
(hx : x ∈ Ring.jacobson R)
(y : R)
:
IsUnit (1 - y * x)
Elements of the radical of a Dedekind-finite ring are quasi-regular.
theorem
MultiplicativeBasisDeformations.dedekindFinite
(k : Type u)
[Field k]
(A : Type v)
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
:
IsDedekindFiniteMonoid A
def
MultiplicativeBasisDeformations.cornerValL
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
{e : A}
(he : IsIdempotentElem e)
:
he.Corner →ₗ[k] A
The value map of the corner, as a k-linear map.
Instances For
theorem
MultiplicativeBasisDeformations.cornerValL_apply
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(he : IsIdempotentElem e)
(x : he.Corner)
:
(cornerValL k he) x = cornerVal he x
theorem
MultiplicativeBasisDeformations.cornerVal_mem_jacobson
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(he : IsIdempotentElem e)
{x : he.Corner}
(hx : x ∈ Ring.jacobson he.Corner)
:
cornerVal he x ∈ Ring.jacobson A
theorem
MultiplicativeBasisDeformations.cornerMk_mem_jacobson
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(he : IsIdempotentElem e)
{z : A}
(hz : z ∈ Ring.jacobson A)
(hze : z ∈ Subsemigroup.corner e)
:
cornerMk he z hze ∈ Ring.jacobson he.Corner
theorem
MultiplicativeBasisDeformations.cornerVal_mem_radPow
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(he : IsIdempotentElem e)
{m : ℕ}
(hm : 1 ≤ m)
{x : he.Corner}
(hx : x ∈ algebraRadicalPow k he.Corner m)
:
cornerVal he x ∈ algebraRadicalPow k A m
(rad eAe)^m ⊆ (rad A)^m.
theorem
MultiplicativeBasisDeformations.corner_mem_radPow
(k : Type u)
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(he : IsIdempotentElem e)
(hfull : 1 ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q})
{m : ℕ}
(hm : 1 ≤ m)
{z : A}
(hz : z ∈ algebraRadicalPow k A m)
(p' q' : A)
:
e * p' * z * q' * e ∈ Submodule.map (cornerValL k he) (algebraRadicalPow k he.Corner m)
e (rad A)^m e ⊆ (rad eAe)^m when AeA = A: insert 1 ∈ AeA between
the factors.