Scalar automorphisms on group-like elements of base-changed bialgebras

For a commutative semiring extension L/K and a K-bialgebra A, the scalar-factor action on L ⊗[K] A preserves the counit and comultiplication equations defining group-like elements. It therefore induces an action on the group-like elements, and Additive.distribMulAction transports that action to their additive form.

Main declarations

• TauCeti.ScalarAut.isGroupLikeElem_smul: scalar automorphisms preserve group-like elements.
• TauCeti.ScalarAut.groupLikeMap_smul: the induced map on group-like elements is equivariant.
• TauCeti.ScalarAut.instGroupLikeDistribMulAction: the induced action on group-like elements.
• BialgHom.map_smul_iff_groupLike: equivariance can be checked on spanning group-like elements.

theorem TauCeti.ScalarAut.counit_smul {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] (σ : L ≃ₐ[K] L) (x : TensorProduct K L A) : CoalgebraStruct.counit (σ • x) = σ (CoalgebraStruct.counit x)

The counit is equivariant for the semilinear scalar action.

theorem TauCeti.ScalarAut.comul_smul {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] (σ : L ≃ₐ[K] L) (x : TensorProduct K L A) : CoalgebraStruct.comul (σ • x) = (TensorProduct.map (semilinearMap σ) (semilinearMap σ)) (CoalgebraStruct.comul x)

Comultiplication is equivariant for the semilinear scalar action.

theorem TauCeti.ScalarAut.isGroupLikeElem_smul {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] (σ : L ≃ₐ[K] L) {x : TensorProduct K L A} (hx : IsGroupLikeElem L x) : IsGroupLikeElem L (σ • x)

Applying a scalar automorphism preserves the group-like equations.

@[instance_reducible]

noncomputable instance TauCeti.ScalarAut.instGroupLikeDistribMulAction {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] : MulDistribMulAction (L ≃ₐ[K] L) (GroupLike L (TensorProduct K L A))

Scalar automorphisms act multiplicatively on group-like elements.

Equations

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

@[simp]

theorem TauCeti.ScalarAut.val_smul {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] (σ : L ≃ₐ[K] L) (x : GroupLike L (TensorProduct K L A)) : ↑(σ • x) = σ • ↑x

The value of the scalar action on a group-like element is the scalar-factor action.

@[simp]

theorem TauCeti.ScalarAut.groupLikeMap_smul {K : Type u} {L : Type v} {A : Type w} [CommSemiring K] [CommSemiring L] [Algebra K L] [Semiring A] [Bialgebra K A] {B : Type u_1} [Semiring B] [Bialgebra K B] (f : A →ₐc[K] B) (σ : L ≃ₐ[K] L) (x : GroupLike L (TensorProduct K L A)) : (GroupLike.map (Bialgebra.TensorProduct.map (BialgHom.id L L) f)) (σ • x) = σ • (GroupLike.map (Bialgebra.TensorProduct.map (BialgHom.id L L) f)) x

The map on group-like elements induced by scalar extension is equivariant for scalar automorphisms.

theorem BialgHom.map_smul_iff_groupLike {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring k] [CommSemiring L] [Algebra k L] [Semiring A] [Bialgebra k A] [Semiring B] [Bialgebra k B] (f : TensorProduct k L A →ₐc[L] TensorProduct k L B) (hA : Submodule.span L (Set.range GroupLike.val) = ⊤) (σ : L ≃ₐ[k] L) : (∀ (x : TensorProduct k L A), f (σ • x) = σ • f x) ↔ ∀ (x : GroupLike L (TensorProduct k L A)), (TauCeti.GroupLike.map f) (σ • x) = σ • (TauCeti.GroupLike.map f) x

A map out of a scalar extension spanned by group-like elements commutes with a scalar automorphism exactly when its restriction to group-like elements does.