Cancelling a regular summand of S²

Let S be a semisimple ring. If v : S² generates a copy of the regular module, that is, if x ↦ x v is injective on S, then the quotient S² / S v is again isomorphic to S. The submodule S v has a complement Q because every module over a semisimple ring is semisimple, so that S × Q ≃ S × S; since S has finite length as a module over itself, the Krull–Schmidt cancellation theorem gives Q ≃ S. For the group algebra k[G] of a finite group over a field in which #G is invertible, the semisimplicity is Maschke's theorem.

The second result applies this after a flat base change. Let A be an algebra over a commutative ring R, and Q a flat R-algebra such that A ⊗[R] Q is semisimple — A = ℤ_p[G] and Q = ℚ_p for a finite group G, say. If v : A² generates a copy of A, then the base change (A² / A v) ⊗[R] Q is isomorphic to A ⊗[R] Q as a left A-module: tensoring is right exact, so the base change of A² / A v is (A ⊗[R] Q)² / (A ⊗[R] Q) v, and flatness carries the injectivity of x ↦ x v to A ⊗[R] Q, where the first result applies.

Main statements

• TauCeti.nonempty_quotient_span_singleton_linearEquiv_of_injective: over a semisimple ring, the quotient of S² by an injectively generated singleton relation is linearly equivalent to S.
• TauCeti.nonempty_quotient_span_singleton_tensor_linearEquiv_of_injective: the base change of A² / A v along a flat R-algebra Q with A ⊗[R] Q semisimple is A ⊗[R] Q.

theorem TauCeti.nonempty_quotient_span_singleton_linearEquiv_of_injective {S : Type u_1} [Ring S] [IsSemisimpleRing S] (v : Fin 2 →₀ S) (hinj : Function.Injective ⇑(LinearMap.toSpanSingleton S (Fin 2 →₀ S) v)) : Nonempty (((Fin 2 →₀ S) ⧸ S ∙ v) ≃ₗ[S] S)

Let S be a semisimple ring. If the singleton relation generated by v : S² is a copy of the regular module, then its quotient is also linearly equivalent to the regular module.

theorem TauCeti.nonempty_quotient_span_singleton_tensor_linearEquiv_of_injective {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] (Q : Type u_3) [Ring Q] [Algebra R Q] [Module.Flat R Q] [IsSemisimpleRing (TensorProduct R A Q)] (v : Fin 2 →₀ A) (hinj : Function.Injective ⇑(LinearMap.toSpanSingleton A (Fin 2 →₀ A) v)) : Nonempty (TensorProduct R ((Fin 2 →₀ A) ⧸ A ∙ v) Q ≃ₗ[A] TensorProduct R A Q)

Cancelling a regular summand after a flat base change. Let A be an algebra over the commutative ring R, and Q a flat R-algebra such that A ⊗[R] Q is a semisimple ring. If v : A² generates a copy of A, then the base change (A² ⧸ A v) ⊗[R] Q is isomorphic to A ⊗[R] Q as a left A-module.