Group actions on embeddings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides a mul_action G (α ↪ β) instance that agrees with the mul_action G (α → β)
instances defined by pi.mul_action.
Note that unlike the pi instance, this requires G to be a group.
@[protected, instance]
def
function.embedding.has_smul
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[group G]
[mul_action G β] :
Equations
- function.embedding.has_smul = {smul := λ (g : G) (f : α ↪ β), f.trans (equiv.to_embedding (mul_action.to_perm g))}
@[protected, instance]
def
function.embedding.has_vadd
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[add_group G]
[add_action G β] :
Equations
- function.embedding.has_vadd = {vadd := λ (g : G) (f : α ↪ β), f.trans (equiv.to_embedding (add_action.to_perm g))}
theorem
function.embedding.vadd_def
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[add_group G]
[add_action G β]
(g : G)
(f : α ↪ β) :
g +ᵥ f = f.trans (equiv.to_embedding (add_action.to_perm g))
theorem
function.embedding.smul_def
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[group G]
[mul_action G β]
(g : G)
(f : α ↪ β) :
g • f = f.trans (equiv.to_embedding (mul_action.to_perm g))
@[protected, instance]
def
function.embedding.is_scalar_tower
{G : Type u_1}
{G' : Type u_2}
{α : Type u_3}
{β : Type u_4}
[group G]
[group G']
[has_smul G G']
[mul_action G β]
[mul_action G' β]
[is_scalar_tower G G' β] :
is_scalar_tower G G' (α ↪ β)
@[protected, instance]
def
function.embedding.vadd_comm_class
{G : Type u_1}
{G' : Type u_2}
{α : Type u_3}
{β : Type u_4}
[add_group G]
[add_group G']
[add_action G β]
[add_action G' β]
[vadd_comm_class G G' β] :
vadd_comm_class G G' (α ↪ β)
@[protected, instance]
def
function.embedding.smul_comm_class
{G : Type u_1}
{G' : Type u_2}
{α : Type u_3}
{β : Type u_4}
[group G]
[group G']
[mul_action G β]
[mul_action G' β]
[smul_comm_class G G' β] :
smul_comm_class G G' (α ↪ β)
@[protected, instance]
def
function.embedding.is_central_scalar
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[group G]
[mul_action G β]
[mul_action Gᵐᵒᵖ β]
[is_central_scalar G β] :
is_central_scalar G (α ↪ β)
@[protected, instance]
def
function.embedding.mul_action
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[group G]
[mul_action G β] :
mul_action G (α ↪ β)
Equations
- function.embedding.mul_action = function.injective.mul_action coe_fn function.embedding.mul_action._proof_1 function.embedding.coe_smul
@[protected, instance]
def
function.embedding.add_action
{G : Type u_1}
{α : Type u_3}
{β : Type u_4}
[add_group G]
[add_action G β] :
add_action G (α ↪ β)
Equations
- function.embedding.add_action = function.injective.add_action coe_fn function.embedding.add_action._proof_1 function.embedding.coe_vadd