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

Function.Embedding.vadd = { vadd := fun g f => Function.Embedding.trans f (Equiv.toEmbedding (AddAction.toPerm g)) }

instance Function.Embedding.smul {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst : MulAction G β] :

SMul G (α ↪ β)

Equations

Function.Embedding.smul = { smul := fun 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_2} [inst : AddGroup G] [inst : 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_2} [inst : Group G] [inst : 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_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

@Function.Embedding.instIsScalarTowerEmbeddingSmulSmul = @Function.Embedding.instIsScalarTowerEmbeddingSmulSmul.proof_1

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

(_ : VAddCommClass G G' (α ↪ β)) = (_ : VAddCommClass G G' (α ↪ β))

instance Function.Embedding.instVAddCommClassEmbeddingVaddVadd {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

@Function.Embedding.instVAddCommClassEmbeddingVaddVadd = @Function.Embedding.instVAddCommClassEmbeddingVaddVadd.proof_1

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

SMulCommClass G G' (α ↪ β)

Equations

@Function.Embedding.instSMulCommClassEmbeddingSmulSmul = @Function.Embedding.instSMulCommClassEmbeddingSmulSmul.proof_1

instance Function.Embedding.instIsCentralScalarEmbeddingSmulMulOppositeGroup {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst : MulAction G β] [inst : MulAction Gᵐᵒᵖ β] [inst : IsCentralScalar G β] :

IsCentralScalar G (α ↪ β)

Equations

@Function.Embedding.instIsCentralScalarEmbeddingSmulMulOppositeGroup = @Function.Embedding.instIsCentralScalarEmbeddingSmulMulOppositeGroup.proof_1

def Function.Embedding.instAddActionEmbeddingToAddMonoidToSubNegAddMonoid.proof_1 {α : Type u_1} {β : Type u_2} :

Function.Injective fun f => ↑f

Equations

(_ : Function.Injective fun f => ↑f) = (_ : Function.Injective fun f => ↑f)

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.