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_3} {β : Type u_4} [AddGroup G] [AddAction G β] : VAdd G (α ↪ β)

Equations

• Function.Embedding.vadd = { vadd := fun (g : G) (f : α ↪ β) => Function.Embedding.trans f (Equiv.toEmbedding (AddAction.toPerm g)) }

instance Function.Embedding.smul {G : Type u_1} {α : Type u_3} {β : Type u_4} [Group G] [MulAction G β] : SMul G (α ↪ β)

Equations

• Function.Embedding.smul = { smul := fun (g : G) (f : α ↪ β) => Function.Embedding.trans f (Equiv.toEmbedding (MulAction.toPerm g)) }

theorem Function.Embedding.vadd_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddAction G β] (g : G) (f : α ↪ β) : g +ᵥ f = Function.Embedding.trans f (Equiv.toEmbedding (AddAction.toPerm g))

theorem Function.Embedding.smul_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [Group G] [MulAction G β] (g : G) (f : α ↪ β) : g • f = Function.Embedding.trans f (Equiv.toEmbedding (MulAction.toPerm g))

@[simp]

theorem Function.Embedding.vadd_apply {G : Type u_1} {α : Type u_3} {β : Type u_4} [AddGroup G] [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_4} [Group G] [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_4} [AddGroup G] [AddAction G β] (g : G) (f : α ↪ β) : ⇑(g +ᵥ f) = g +ᵥ ⇑f

theorem Function.Embedding.coe_smul {G : Type u_1} {α : Type u_3} {β : Type u_4} [Group G] [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} [Group G] [Group G'] [SMul G G'] [MulAction G β] [MulAction G' β] [IsScalarTower G G' β] : IsScalarTower G G' (α ↪ β)

Equations

• ⋯ = ⋯

instance Function.Embedding.instVAddCommClassEmbeddingVaddVadd {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddGroup G'] [AddAction G β] [AddAction G' β] [VAddCommClass G G' β] : VAddCommClass G G' (α ↪ β)

Equations

• ⋯ = ⋯

instance Function.Embedding.instSMulCommClassEmbeddingSmulSmul {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [Group G] [Group G'] [MulAction G β] [MulAction G' β] [SMulCommClass G G' β] : SMulCommClass G G' (α ↪ β)

Equations

• ⋯ = ⋯

instance Function.Embedding.instIsCentralScalarEmbeddingSmulMulOppositeGroup {G : Type u_1} {α : Type u_3} {β : Type u_4} [Group G] [MulAction G β] [MulAction Gᵐᵒᵖ β] [IsCentralScalar G β] : IsCentralScalar G (α ↪ β)

Equations

• ⋯ = ⋯

instance Function.Embedding.instAddActionEmbeddingToAddMonoidToSubNegAddMonoid {G : Type u_1} {α : Type u_3} {β : Type u_4} [AddGroup G] [AddAction G β] : AddAction G (α ↪ β)

Equations

• Function.Embedding.instAddActionEmbeddingToAddMonoidToSubNegAddMonoid = Function.Injective.addAction (fun (f : α ↪ β) => ⇑f) ⋯ ⋯

theorem Function.Embedding.instAddActionEmbeddingToAddMonoidToSubNegAddMonoid.proof_1 {α : Type u_1} {β : Type u_2} : Function.Injective fun (f : α ↪ β) => ⇑f

instance Function.Embedding.instMulActionEmbeddingToMonoidToDivInvMonoid {G : Type u_1} {α : Type u_3} {β : Type u_4} [Group G] [MulAction G β] : MulAction G (α ↪ β)

Equations

• Function.Embedding.instMulActionEmbeddingToMonoidToDivInvMonoid = Function.Injective.mulAction (fun (f : α ↪ β) => ⇑f) ⋯ ⋯