An algebra as a module over B ⊗[K] Aᵐᵒᵖ

A K-algebra homomorphism f : B →ₐ[K] A turns A into a B-A-bimodule: B acts on the left through f and A on the right by multiplication. Packaged as a left module over R = B ⊗[K] Aᵐᵒᵖ, with b ⊗ₜ op a acting by x ↦ f b * x * a, this is TauCeti.Bimodule f.

Two theorems rest on this one construction, and neither can use A itself as the carrier:

• the Skolem-Noether theorem (TauCeti/Algebra/CentralSimple/SkolemNoether.lean) compares the structures coming from two homomorphisms f and g on the same underlying K-vector space, so the two module structures must coexist;
• the centralizer theorem (TauCeti/Algebra/CentralSimple/Centralizer.lean) identifies the endomorphism ring of Bimodule f with the centralizer of the image of f, and needs A to carry no competing R-module structure while it does so.

Indexing a type synonym by the homomorphism answers both: the structures are separated by f, and none of them is an instance on A. Mathlib takes the same route for A ⊗[R] Aᵐᵒᵖ acting on A in Mathlib/Algebra/Azumaya/Defs.lean, where instModuleTensorProductMop is deliberately not an instance.

Main definitions

• TauCeti.Bimodule f: the type synonym, with its B ⊗[K] Aᵐᵒᵖ-module structure.
• TauCeti.Bimodule.of f : A ≃ₗ[K] Bimodule f: the identification with A as a K-module, the only route between the two types that the interface offers.
• TauCeti.Bimodule.toEnd f: the action, as a K-algebra homomorphism into Module.End K A. It is Mathlib's AlgHom.mulLeftRight restricted along f on the left factor, so for f = AlgHom.id K A it is AlgHom.mulLeftRight K A itself.

A B ⊗[K] Aᵐᵒᵖ-linear map Bimodule f →ₗ Bimodule g, transported along of, is determined by its value u at 1, and that value intertwines f and g:

• TauCeti.Bimodule.symm_apply_eq_symm_apply_one_mul: the transported map is a ↦ u * a.
• TauCeti.Bimodule.apply_of: the untransported form, φ (of f a) = of g (u * a).
• TauCeti.Bimodule.symm_apply_one_mul_eq_mul_symm_apply_one: u * f b = g b * u.
• TauCeti.Bimodule.exists_symm_apply_one_mul_eq_one: when of g 1 is hit, u has a right inverse.

The two consumers take different halves. The Skolem-Noether argument in TauCeti/Algebra/CentralSimple/SkolemNoether.lean uses the right-inverse lemma exists_symm_apply_one_mul_eq_one and the intertwining lemma symm_apply_one_mul_eq_mul_symm_apply_one; the centralizer theorem in TauCeti/Algebra/CentralSimple/Centralizer.lean uses apply_of and the same intertwining lemma, at f = g = B.val.

More generally, Bimodule f is generated by 1 subject only to b • 1 = 1 • f b, and this is its universal property among all B ⊗[K] Aᵐᵒᵖ-modules M:

• TauCeti.Bimodule.eq_of_apply_one_eq: a B ⊗[K] Aᵐᵒᵖ-linear map Bimodule f → M is determined by its value at 1.
• TauCeti.Bimodule.lift: every c : M on which b ⊗ₜ 1 and 1 ⊗ₜ op (f b) act alike is the value at 1 of such a map, a ↦ (1 ⊗ₜ op a) • c. For f = AlgHom.id K A these are the maps of A-bimodules out of A, such as the coevaluation of a symmetric Frobenius algebra.

Implementation notes

TauCeti.Bimodule.smul_of and TauCeti.Bimodule.symm_smul are the working interface: they compute the action of a pure tensor on either side of of, and every consumer is expected to reach the module structure through them and through TauCeti.Bimodule.smul_def rather than by unfolding the synonym. Only Bimodule is @[expose]d, and it has to be: a type synonym cannot carry transported instances unless its body is visible. Everything else, of and toEnd included, stays opaque, so that no consumer can depend on their bodies; smul_def is proved by (rfl) rather than by rfl, which is what keeps it from being tagged @[defeq] — an exported @[defeq] theorem would demand that the body of of be exposed too.

Nothing in the construction uses negation, so A and B are asked only to be semirings; the additive group structure is inherited conditionally, when A happens to be a ring.

References

This is the shared construction beneath the Layer 5 targets skolemNoether and finrank_mul_finrank_centralizer of the semisimple algebras roadmap. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12.

def TauCeti.Bimodule {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (_f : B →ₐ[K] A) : Type u_2

A regarded as a left module over B ⊗[K] Aᵐᵒᵖ through an algebra homomorphism f : B →ₐ[K] A: the element b ⊗ₜ op a acts by x ↦ f b * x * a.

Equivalently this is the B-A-bimodule A obtained by restricting the left action along f, packaged as a left module over B ⊗[K] Aᵐᵒᵖ in the usual way. It is a type synonym for A precisely so that the structures coming from two different homomorphisms can be compared, and so that A itself is left without a B ⊗[K] Aᵐᵒᵖ-action.

Equations

• TauCeti.Bimodule _f = A

@[instance_reducible]

instance TauCeti.Bimodule.instAddCommMonoid {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : AddCommMonoid (Bimodule f)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.Bimodule.instAddCommGroup {K : Type u_1} {B : Type u_3} [CommSemiring K] [Semiring B] [Algebra K B] {A : Type u_4} [Ring A] [Algebra K A] (f : B →ₐ[K] A) : AddCommGroup (Bimodule f)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.Bimodule.instModule {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : Module K (Bimodule f)

Equations

• TauCeti.Bimodule.instModule f = { toSMul := TauCeti.Bimodule.instModule._aux_1 f, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance TauCeti.Bimodule.instNontrivial {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) [Nontrivial A] : Nontrivial (Bimodule f)

def TauCeti.Bimodule.of {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : A ≃ₗ[K] Bimodule f

Bimodule f is A again as a K-module: only the B ⊗[K] Aᵐᵒᵖ-action is new.

Equations

• TauCeti.Bimodule.of f = LinearEquiv.refl K A

noncomputable def TauCeti.Bimodule.toEnd {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : TensorProduct K B Aᵐᵒᵖ →ₐ[K] Module.End K A

The action of B ⊗[K] Aᵐᵒᵖ on A defining Bimodule f, as an algebra homomorphism into Module.End K A. It is Mathlib's AlgHom.mulLeftRight restricted along f on the left factor, so for f = AlgHom.id K A it is AlgHom.mulLeftRight K A itself.

Equations

• TauCeti.Bimodule.toEnd f = (AlgHom.mulLeftRight K A).comp (Algebra.TensorProduct.map f (AlgHom.id K Aᵐᵒᵖ))

@[simp]

theorem TauCeti.Bimodule.toEnd_tmul_apply {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) (b : B) (a : Aᵐᵒᵖ) (x : A) : ((toEnd f) (b ⊗ₜ[K] a)) x = f b * x * MulOpposite.unop a

A pure tensor b ⊗ₜ op a acts on x : A through toEnd f by x ↦ f b * x * a.

@[instance_reducible]

noncomputable instance TauCeti.Bimodule.instModuleTensorProductMulOpposite {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : Module (TensorProduct K B Aᵐᵒᵖ) (Bimodule f)

Equations

• TauCeti.Bimodule.instModuleTensorProductMulOpposite f = Module.compHom A (TauCeti.Bimodule.toEnd f).toRingHom

theorem TauCeti.Bimodule.smul_def {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) (r : TensorProduct K B Aᵐᵒᵖ) (x : A) : r • (of f) x = (of f) (((toEnd f) r) x)

A scalar r : B ⊗[K] Aᵐᵒᵖ acts on Bimodule f through toEnd f. This is the defining equation of the module structure, and the single place it is unfolded: everything else below rewrites with it instead of reasoning up to definitional equality.

instance TauCeti.Bimodule.instIsScalarTowerTensorProductMulOpposite {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) : IsScalarTower K (TensorProduct K B Aᵐᵒᵖ) (Bimodule f)

instance TauCeti.Bimodule.instFinite {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) [Module.Finite K A] : Module.Finite K (Bimodule f)

@[simp]

theorem TauCeti.Bimodule.smul_of {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) (b : B) (a : Aᵐᵒᵖ) (x : A) : b ⊗ₜ[K] a • (of f) x = (of f) (f b * x * MulOpposite.unop a)

A pure tensor b ⊗ₜ op a acts on Bimodule f by x ↦ f b * x * a: the left factor acts on the left through f, the right factor on the right by multiplication.

@[simp]

theorem TauCeti.Bimodule.symm_smul {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) (b : B) (a : Aᵐᵒᵖ) (y : Bimodule f) : (of f).symm (b ⊗ₜ[K] a • y) = f b * (of f).symm y * MulOpposite.unop a

smul_of read back through of: the action of a pure tensor b ⊗ₜ op a, transported to A, is x ↦ f b * x * a.

theorem TauCeti.Bimodule.symm_apply_eq_symm_apply_one_mul {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] {f g : B →ₐ[K] A} (φ : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] Bimodule g) (a : A) : (of g).symm (φ ((of f) a)) = (of g).symm (φ ((of f) 1)) * a

Transported along Bimodule.of, a B ⊗[K] Aᵐᵒᵖ-linear map Bimodule f →ₗ Bimodule g sends a to its value at 1, multiplied by a.

theorem TauCeti.Bimodule.apply_of {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] {f g : B →ₐ[K] A} (φ : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] Bimodule g) (a : A) : φ ((of f) a) = (of g) ((of g).symm (φ ((of f) 1)) * a)

The untransported form of symm_apply_eq_symm_apply_one_mul: φ sends of f a to of g (u * a), where u is its transported value at 1. This is the of-side companion, in the same way that smul_of is the companion of symm_smul.

theorem TauCeti.Bimodule.symm_apply_one_mul_eq_mul_symm_apply_one {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] {f g : B →ₐ[K] A} (φ : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] Bimodule g) (b : B) : (of g).symm (φ ((of f) 1)) * f b = g b * (of g).symm (φ ((of f) 1))

The transported value at 1 intertwines f and g: writing u for it, u * f b = g b * u for every b : B.

theorem TauCeti.Bimodule.exists_symm_apply_one_mul_eq_one {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] {f g : B →ₐ[K] A} (φ : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] Bimodule g) (h1 : (of g) 1 ∈ φ.range) : ∃ (v : A), (of g).symm (φ ((of f) 1)) * v = 1

Whenever of g 1 is in the range of φ, the transported value at 1 has a right inverse in A. Surjectivity of φ is more than is needed: only this one value must be hit.

theorem TauCeti.Bimodule.eq_of_apply_one_eq {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] {f : B →ₐ[K] A} {M : Type u_4} [AddCommMonoid M] [Module (TensorProduct K B Aᵐᵒᵖ) M] {φ ψ : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] M} (h : φ ((of f) 1) = ψ ((of f) 1)) : φ = ψ

A B ⊗[K] Aᵐᵒᵖ-linear map out of Bimodule f is determined by its value at 1.

noncomputable def TauCeti.Bimodule.lift {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) {M : Type u_4} [AddCommMonoid M] [Module (TensorProduct K B Aᵐᵒᵖ) M] (c : M) (hc : ∀ (b : B), b ⊗ₜ[K] 1 • c = 1 ⊗ₜ[K] MulOpposite.op (f b) • c) : Bimodule f →ₗ[TensorProduct K B Aᵐᵒᵖ] M

The universal property of Bimodule f. An element c of a B ⊗[K] Aᵐᵒᵖ-module on which b ⊗ₜ 1 and 1 ⊗ₜ op (f b) act alike for every b : B is the value at 1 of the B ⊗[K] Aᵐᵒᵖ-linear map Bimodule f → M sending a to (1 ⊗ₜ op a) • c. Conversely the value at 1 of any such map satisfies the hypothesis, and determines the map by Bimodule.eq_of_apply_one_eq.

Equations

• TauCeti.Bimodule.lift f c hc = { toFun := fun (x : TauCeti.Bimodule f) => 1 ⊗ₜ[K] MulOpposite.op ((TauCeti.Bimodule.of f).symm x) • c, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Bimodule.lift_of {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) {M : Type u_4} [AddCommMonoid M] [Module (TensorProduct K B Aᵐᵒᵖ) M] (c : M) (hc : ∀ (b : B), b ⊗ₜ[K] 1 • c = 1 ⊗ₜ[K] MulOpposite.op (f b) • c) (a : A) : (lift f c hc) ((of f) a) = 1 ⊗ₜ[K] MulOpposite.op a • c

Bimodule.lift f c hc sends a to (1 ⊗ₜ op a) • c.

@[simp]

theorem TauCeti.Bimodule.lift_of_one {K : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (f : B →ₐ[K] A) {M : Type u_4} [AddCommMonoid M] [Module (TensorProduct K B Aᵐᵒᵖ) M] (c : M) (hc : ∀ (b : B), b ⊗ₜ[K] 1 • c = 1 ⊗ₜ[K] MulOpposite.op (f b) • c) : (lift f c hc) ((of f) 1) = c

Bimodule.lift f c hc sends 1 to c.