Documentation

Mathlib.GroupTheory.GroupAction.Embedding

Group actions on embeddings #

This file provides a MulAction G (α ↪ β) instance that agrees with the MulAction G (α → β) instances defined by Pi.mulAction.

Note that unlike the Pi instance, this requires G to be a group.

instance Function.Embedding.vadd {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst : AddAction G β] :
VAdd G (α β)
Equations
instance Function.Embedding.smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst : MulAction G β] :
SMul G (α β)
Equations
theorem Function.Embedding.vadd_def {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : AddGroup G] [inst : AddAction G β] (g : G) (f : α β) :
theorem Function.Embedding.smul_def {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : Group G] [inst : MulAction G β] (g : G) (f : α β) :
@[simp]
theorem Function.Embedding.vadd_apply {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : AddGroup G] [inst : AddAction G β] (g : G) (f : α β) (a : α) :
↑(g +ᵥ f) a = g +ᵥ f a
@[simp]
theorem Function.Embedding.smul_apply {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : Group G] [inst : MulAction G β] (g : G) (f : α β) (a : α) :
↑(g f) a = g f a
theorem Function.Embedding.coe_vadd {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : AddGroup G] [inst : AddAction G β] (g : G) (f : α β) :
↑(g +ᵥ f) = g +ᵥ f
theorem Function.Embedding.coe_smul {G : Type u_1} {α : Type u_3} {β : Type u_2} [inst : Group G] [inst : MulAction G β] (g : G) (f : α β) :
↑(g f) = g f
instance Function.Embedding.instIsScalarTowerEmbeddingSmulSmul {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst : Group G'] [inst : SMul G G'] [inst : MulAction G β] [inst : MulAction G' β] [inst : IsScalarTower G G' β] :
IsScalarTower G G' (α β)
Equations
def Function.Embedding.instVAddCommClassEmbeddingVaddVadd.proof_1 {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst : AddGroup G'] [inst : AddAction G β] [inst : AddAction G' β] [inst : VAddCommClass G G' β] :
VAddCommClass G G' (α β)
Equations
instance Function.Embedding.instAddActionEmbeddingToAddMonoidToSubNegAddMonoid {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup G] [inst : AddAction G β] :
AddAction G (α β)
Equations
  • One or more equations did not get rendered due to their size.
instance Function.Embedding.instMulActionEmbeddingToMonoidToDivInvMonoid {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst : MulAction G β] :
MulAction G (α β)
Equations
  • One or more equations did not get rendered due to their size.