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 β]
:
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 β]
:
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))
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' (α ↪ β)
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' (α ↪ β)
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' (α ↪ β)
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 (α ↪ β)
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)