mathlib documentation

group_theory.group_action.pi

Pi instances for multiplicative actions #

This file defines instances for mul_action and related structures on Pi Types

source
@[protected, instance]
def pi.has_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] :
has_vadd α (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.has_scalar {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] :
has_scalar α (Π (i : I), f i)
Equations
source
theorem pi.vadd_def {I : Type u} {f : I → Type v} (x : Π (i : I), f i) {α : Type u_1} [Π (i : I), has_vadd α (f i)] (s : α) :
s +ᵥ x = λ (i : I), s +ᵥ x i
source
theorem pi.smul_def {I : Type u} {f : I → Type v} (x : Π (i : I), f i) {α : Type u_1} [Π (i : I), has_scalar α (f i)] (s : α) :
s • x = λ (i : I), s • x i
source
@[simp]
theorem pi.vadd_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) {α : Type u_1} [Π (i : I), has_vadd α (f i)] (s : α) :
(s +ᵥ x) i = s +ᵥ x i
source
@[simp]
theorem pi.smul_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) {α : Type u_1} [Π (i : I), has_scalar α (f i)] (s : α) :
(s • x) i = s • x i
source
@[protected, instance]
def pi.has_vadd' {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), has_vadd (f i) (g i)] :
has_vadd (Π (i : I), f i) (Π (i : I), g i)
Equations
source
@[protected, instance]
def pi.has_scalar' {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), has_scalar (f i) (g i)] :
has_scalar (Π (i : I), f i) (Π (i : I), g i)
Equations
source
@[simp]
theorem pi.vadd_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [Π (i : I), has_vadd (f i) (g i)] (s : Π (i : I), f i) (x : Π (i : I), g i) :
(s +ᵥ x) i = s i +ᵥ x i
source
@[simp]
theorem pi.smul_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [Π (i : I), has_scalar (f i) (g i)] (s : Π (i : I), f i) (x : Π (i : I), g i) :
(s • x) i = s i • x i
source
@[protected, instance]
def pi.is_scalar_tower {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [has_scalar α β] [Π (i : I), has_scalar β (f i)] [Π (i : I), has_scalar α (f i)] [∀ (i : I), is_scalar_tower α β (f i)] :
is_scalar_tower α β (Π (i : I), f i)
source
@[protected, instance]
def pi.is_scalar_tower' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [Π (i : I), has_scalar α (f i)] [Π (i : I), has_scalar (f i) (g i)] [Π (i : I), has_scalar α (g i)] [∀ (i : I), is_scalar_tower α (f i) (g i)] :
is_scalar_tower α (Π (i : I), f i) (Π (i : I), g i)
source
@[protected, instance]
def pi.is_scalar_tower'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [Π (i : I), has_scalar (f i) (g i)] [Π (i : I), has_scalar (g i) (h i)] [Π (i : I), has_scalar (f i) (h i)] [∀ (i : I), is_scalar_tower (f i) (g i) (h i)] :
is_scalar_tower (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
source
@[protected, instance]
def pi.smul_comm_class {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [Π (i : I), has_scalar α (f i)] [Π (i : I), has_scalar β (f i)] [∀ (i : I), smul_comm_class α β (f i)] :
smul_comm_class α β (Π (i : I), f i)
source
@[protected, instance]
def pi.vadd_comm_class {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [Π (i : I), has_vadd α (f i)] [Π (i : I), has_vadd β (f i)] [∀ (i : I), vadd_comm_class α β (f i)] :
vadd_comm_class α β (Π (i : I), f i)
source
@[protected, instance]
def pi.smul_comm_class' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [Π (i : I), has_scalar α (g i)] [Π (i : I), has_scalar (f i) (g i)] [∀ (i : I), smul_comm_class α (f i) (g i)] :
smul_comm_class α (Π (i : I), f i) (Π (i : I), g i)
source
@[protected, instance]
def pi.vadd_comm_class' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [Π (i : I), has_vadd α (g i)] [Π (i : I), has_vadd (f i) (g i)] [∀ (i : I), vadd_comm_class α (f i) (g i)] :
vadd_comm_class α (Π (i : I), f i) (Π (i : I), g i)
source
@[protected, instance]
def pi.smul_comm_class'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [Π (i : I), has_scalar (g i) (h i)] [Π (i : I), has_scalar (f i) (h i)] [∀ (i : I), smul_comm_class (f i) (g i) (h i)] :
smul_comm_class (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
source
@[protected, instance]
def pi.vadd_comm_class'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [Π (i : I), has_vadd (g i) (h i)] [Π (i : I), has_vadd (f i) (h i)] [∀ (i : I), vadd_comm_class (f i) (g i) (h i)] :
vadd_comm_class (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
source
@[protected, instance]
def pi.is_central_scalar {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] [Π (i : I), has_scalar αᵐᵒᵖ (f i)] [∀ (i : I), is_central_scalar α (f i)] :
is_central_scalar α (Π (i : I), f i)
source
theorem pi.has_faithful_vadd_at {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] [∀ (i : I), nonempty (f i)] (i : I) [has_faithful_vadd α (f i)] :
has_faithful_vadd α (Π (i : I), f i)
source
theorem pi.has_faithful_scalar_at {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] [∀ (i : I), nonempty (f i)] (i : I) [has_faithful_scalar α (f i)] :
has_faithful_scalar α (Π (i : I), f i)

If f i has a faithful scalar action for a given i, then so does Π i, f i. This is not an instance as i cannot be inferred.

source
@[protected, instance]
def pi.has_faithful_scalar {I : Type u} {f : I → Type v} {α : Type u_1} [nonempty I] [Π (i : I), has_scalar α (f i)] [∀ (i : I), nonempty (f i)] [∀ (i : I), has_faithful_scalar α (f i)] :
has_faithful_scalar α (Π (i : I), f i)
source
@[protected, instance]
def pi.has_faithful_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [nonempty I] [Π (i : I), has_vadd α (f i)] [∀ (i : I), nonempty (f i)] [∀ (i : I), has_faithful_vadd α (f i)] :
has_faithful_vadd α (Π (i : I), f i)
source
@[protected, instance]
def pi.add_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : add_monoid α} [Π (i : I), add_action α (f i)] :
add_action α (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.mul_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : monoid α} [Π (i : I), mul_action α (f i)] :
mul_action α (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.add_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), add_monoid (f i)} [Π (i : I), add_action (f i) (g i)] :
add_action (Π (i : I), f i) (Π (i : I), g i)
Equations
source
@[protected, instance]
def pi.mul_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), monoid (f i)} [Π (i : I), mul_action (f i) (g i)] :
mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
source
@[protected, instance]
def pi.distrib_mul_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : monoid α} {n : Π (i : I), add_monoid (f i)} [Π (i : I), distrib_mul_action α (f i)] :
distrib_mul_action α (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.distrib_mul_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), monoid (f i)} {n : Π (i : I), add_monoid (g i)} [Π (i : I), distrib_mul_action (f i) (g i)] :
distrib_mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
source
theorem pi.single_smul {I : Type u} {f : I → Type v} {α : Type u_1} [monoid α] [Π (i : I), add_monoid (f i)] [Π (i : I), distrib_mul_action α (f i)] [decidable_eq I] (i : I) (r : α) (x : f i) :
pi.single i (r • x) = r • pi.single i x
source
theorem pi.single_smul' {I : Type u} {α : Type u_1} {β : Type u_2} [monoid α] [add_monoid β] [distrib_mul_action α β] [decidable_eq I] (i : I) (r : α) (x : β) :
pi.single i (r • x) = r • pi.single i x

A version of pi.single_smul for non-dependent functions. It is useful in cases Lean fails to apply pi.single_smul.

source
theorem pi.single_smul₀ {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), monoid_with_zero (f i)] [Π (i : I), add_monoid (g i)] [Π (i : I), distrib_mul_action (f i) (g i)] [decidable_eq I] (i : I) (r : f i) (x : g i) :
pi.single i (r • x) = pi.single i r • pi.single i x
source
@[protected, instance]
def pi.mul_distrib_mul_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : monoid α} {n : Π (i : I), monoid (f i)} [Π (i : I), mul_distrib_mul_action α (f i)] :
mul_distrib_mul_action α (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.mul_distrib_mul_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), monoid (f i)} {n : Π (i : I), monoid (g i)} [Π (i : I), mul_distrib_mul_action (f i) (g i)] :
mul_distrib_mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
source
theorem function.update_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] [decidable_eq I] (c : α) (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ function.update f₁ i x₁
source
theorem function.update_smul {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] [decidable_eq I] (c : α) (f₁ : Π (i : I), f i) (i : I) (x₁ : f i) :
function.update (c • f₁) i (c • x₁) = c • function.update f₁ i x₁
source
theorem set.piecewise_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (c : α) (f₁ g₁ : Π (i : I), f i) :
s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁
source
theorem set.piecewise_smul {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] (s : set I) [Π (i : I), decidable (i ∈ s)] (c : α) (f₁ g₁ : Π (i : I), f i) :
s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁
source
theorem function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_scalar R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :
function.extend f (r • g) (r • e) = r • function.extend f g e
source
theorem function.extend_vadd {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :
function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ function.extend f g e