Transport of ray bases

Corollary 5.5 (mesh-deformations.tex): the isomorphism A ≅ A₀ "preserves endpoint actions and the subspaces M(f,h) of Definition 3.4, and therefore identifies ray A with P". Here: an algebra isomorphism matching the chosen primitive idempotents carries corners, corner radicals, corner units, rays and the spaces M(f,h) (ray_fwd, insertionSpan_fwd), hence ray bases (hasRayBasis_of_algEquiv).

The rays are defined relative to a complete set of primitive idempotents. In a basic algebra any two complete sets are conjugate (exists_algEquiv_idempotents), so a ray basis for one set gives one for any other.

theorem MultiplicativeBasisDeformations.IsNormedMultiplicativeBasis.map_algEquiv {k : Type u} [Field k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (φ : A ≃ₐ[k] B) {ι : Type u_1} {b : Module.Basis ι k B} (hb : IsNormedMultiplicativeBasis b) : IsNormedMultiplicativeBasis (b.map ↑φ.symm)

Transport of a normed multiplicative basis along an algebra isomorphism.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.corner_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) {i j : Fin F.m} {a : A} (ha : a ∈ F.corner i j) : ψ a ∈ F'.corner (σ i) (σ j)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.radical_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) {a : A} (ha : a ∈ algebraRadical k A) : ψ a ∈ algebraRadical k B

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.cornerRadical_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) {i : Fin F.m} {a : A} (ha : a ∈ F.cornerRadical i) : ψ a ∈ F'.cornerRadical (σ i)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.unit_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) {i : Fin F.m} {u : A} (hu : F.IsCornerUnit i u) : F'.IsCornerUnit (σ i) (ψ u)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.ray_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) {i j : Fin F.m} {f g : A} (hg : g ∈ F.ray i j f) : ψ g ∈ F'.ray (σ i) (σ j) (ψ f)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.insertionSpan_fwd {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) {i j l : Fin F.m} {f h g : A} (hg : g ∈ F.insertionSpan i j l f h) : ψ g ∈ F'.insertionSpan (σ i) (σ j) (σ l) (ψ f) (ψ h)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.symm_e {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (j : Fin F'.m) : ψ.symm (F'.e j) = F.e (σ.symm j)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.image_ray {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (i j : Fin F.m) (f : A) : ⇑ψ '' F.ray i j f = F'.ray (σ i) (σ j) (ψ f)

def MultiplicativeBasisDeformations.PrimitiveIdempotents.rayMap {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (r : NonzeroRay k F) : NonzeroRay k F'

The image of a nonzero ray.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.rayMap_val {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (r : NonzeroRay k F) : ↑(rayMap ψ F F' σ hψ r) = ⇑ψ '' ↑r

def MultiplicativeBasisDeformations.PrimitiveIdempotents.rayEquiv {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) : NonzeroRay k F ≃ NonzeroRay k F'

Nonzero rays correspond under ψ.

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.hasRayBasis_of_algEquiv {k : Type u} [Field k] [IsAlgClosed k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] [FiniteDimensional k A] [FiniteDimensional k B] (ψ : A ≃ₐ[k] B) (F : PrimitiveIdempotents A) (F' : PrimitiveIdempotents B) (σ : Fin F.m ≃ Fin F'.m) (hψ : ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)) (h : HasRayBasis k F') : HasRayBasis k F

Ray bases transport along an algebra isomorphism matching the idempotents.

def MultiplicativeBasisDeformations.conjAlgEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (W W' : A) (h1 : W * W' = 1) (h2 : W' * W = 1) : A ≃ₐ[k] A

Conjugation a ↦ W' a W by mutually inverse elements.

theorem MultiplicativeBasisDeformations.exists_conj_to {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] {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) (F : PrimitiveIdempotents A) : ∃ (τ : Fin n ≃ Fin F.m) (ψ : A ≃ₐ[k] A), ∀ (j : Fin n), ψ (e j) = F.e (τ j)

A basic set of idempotents is conjugate to any complete set of primitive orthogonal idempotents.

theorem MultiplicativeBasisDeformations.exists_algEquiv_idempotents {k : Type u} [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (hbasic : IsBasicAlgebra A) (F F' : PrimitiveIdempotents A) : ∃ (ψ : A ≃ₐ[k] A) (σ : Fin F.m ≃ Fin F'.m), ∀ (i : Fin F.m), ψ (F.e i) = F'.e (σ i)

In a basic algebra any two complete sets of primitive orthogonal idempotents are conjugate.