mathlib3 documentation

group_theory.group_action.embedding

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