# mathlibdocumentation

group_theory.group_action.embedding

# Group actions on embeddings #

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] [ β] :
β)
Equations
@[protected, instance]
def function.embedding.has_vadd {G : Type u_1} {α : Type u_3} {β : Type u_4} [add_group G] [ β] :
β)
Equations
theorem function.embedding.vadd_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [add_group G] [ β] (g : G) (f : α β) :
g +ᵥ f =
theorem function.embedding.smul_def {G : Type u_1} {α : Type u_3} {β : Type u_4} [group G] [ β] (g : G) (f : α β) :
g f =
@[simp]
theorem function.embedding.smul_apply {G : Type u_1} {α : Type u_3} {β : Type u_4} [group G] [ β] (g : G) (f : α β) (a : α) :
(g f) a = g f a
@[simp]
theorem function.embedding.vadd_apply {G : Type u_1} {α : Type u_3} {β : Type u_4} [add_group G] [ β] (g : G) (f : α β) (a : α) :
(g +ᵥ f) a = g +ᵥ f a
theorem function.embedding.coe_smul {G : Type u_1} {α : Type u_3} {β : Type u_4} [group G] [ β] (g : G) (f : α β) :
(g f) = g f
theorem function.embedding.coe_vadd {G : Type u_1} {α : Type u_3} {β : Type u_4} [add_group G] [ β] (g : G) (f : α β) :
(g +ᵥ f) = g +ᵥ f
@[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'] [ G'] [ β] [ β] [ 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'] [ β] [ β] [ 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'] [ β] [ β] [ G' β] :
G' β)
@[protected, instance]
def function.embedding.is_central_scalar {G : Type u_1} {α : Type u_3} {β : Type u_4} [group G] [ β] [ β] [ β] :
β)
@[protected, instance]
def function.embedding.mul_action {G : Type u_1} {α : Type u_3} {β : Type u_4} [group G] [ β] :
β)
Equations
@[protected, instance]
def function.embedding.add_action {G : Type u_1} {α : Type u_3} {β : Type u_4} [add_group G] [ β] :
β)
Equations