The postcomposition action of algebra equivalences on algebra maps

For algebras L and M over a commutative semiring K, the group M ≃ₐ[K] M acts on the set of algebra maps L →ₐ[K] M by postcomposition, σ • φ = σ ∘ φ.

Only semiring structure is involved, so the action is defined here rather than alongside the field-theoretic facts about it. The orbits and the kernel of this action are what turn a set of embeddings into a group-theoretic object; those statements need fields and live in TauCeti/FieldTheory/Normal/Embeddings.lean.

Main results

• AlgEquiv.smul_algHom_def: the action is postcomposition, σ • φ = σ.toAlgHom.comp φ.
• AlgEquiv.smul_algHom_apply: it evaluates as σ after φ.
• AlgEquiv.apply_of_smul_eq: an equivalence fixing an algebra map fixes its values.

@[instance_reducible]

instance AlgEquiv.smulAlgHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [Semiring L] [Semiring M] [Algebra K L] [Algebra K M] : SMul (M ≃ₐ[K] M) (L →ₐ[K] M)

M ≃ₐ[K] M acts on the algebra maps L →ₐ[K] M by postcomposition.

Equations

• AlgEquiv.smulAlgHom = { smul := fun (σ : M ≃ₐ[K] M) (φ : L →ₐ[K] M) => (↑σ).comp φ }

theorem AlgEquiv.smul_algHom_def {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [Semiring L] [Semiring M] [Algebra K L] [Algebra K M] (σ : M ≃ₐ[K] M) (φ : L →ₐ[K] M) : σ • φ = (↑σ).comp φ

The action is postcomposition.

@[instance_reducible]

instance AlgEquiv.mulActionAlgHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [Semiring L] [Semiring M] [Algebra K L] [Algebra K M] : MulAction (M ≃ₐ[K] M) (L →ₐ[K] M)

Postcomposition makes L →ₐ[K] M an M ≃ₐ[K] M-set.

Equations

• AlgEquiv.mulActionAlgHom = { toSMul := AlgEquiv.smulAlgHom, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem AlgEquiv.smul_algHom_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [Semiring L] [Semiring M] [Algebra K L] [Algebra K M] (σ : M ≃ₐ[K] M) (φ : L →ₐ[K] M) (x : L) : (σ • φ) x = σ (φ x)

The action is evaluation of σ after φ.

theorem AlgEquiv.apply_of_smul_eq {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [Semiring L] [Semiring M] [Algebra K L] [Algebra K M] {σ : M ≃ₐ[K] M} {φ : L →ₐ[K] M} (h : σ • φ = φ) (x : L) : σ (φ x) = φ x

An algebra equivalence fixing an algebra map fixes its values.