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.

See also #

@[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
@[protected, instance]
def pi.has_smul' {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), has_smul (f i) (g i)] :
has_smul (Π (i : I), f i) (Π (i : I), g i)
Equations
@[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
@[simp]
theorem pi.smul_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [Π (i : I), has_smul (f i) (g i)] (s : Π (i : I), f i) (x : Π (i : I), g i) :
(s x) i = s i x i
@[protected, instance]
def pi.is_scalar_tower {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [has_smul α β] [Π (i : I), has_smul β (f i)] [Π (i : I), has_smul α (f i)] [∀ (i : I), is_scalar_tower α β (f i)] :
is_scalar_tower α β (Π (i : I), f i)
@[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_smul α (f i)] [Π (i : I), has_smul (f i) (g i)] [Π (i : I), has_smul α (g i)] [∀ (i : I), is_scalar_tower α (f i) (g i)] :
is_scalar_tower α (Π (i : I), f i) (Π (i : I), g i)
@[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_smul (f i) (g i)] [Π (i : I), has_smul (g i) (h i)] [Π (i : I), has_smul (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)
@[protected, instance]
def pi.smul_comm_class {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [Π (i : I), has_smul α (f i)] [Π (i : I), has_smul β (f i)] [∀ (i : I), smul_comm_class α β (f i)] :
smul_comm_class α β (Π (i : I), f i)
@[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)
@[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_smul α (g i)] [Π (i : I), has_smul (f i) (g i)] [∀ (i : I), smul_comm_class α (f i) (g i)] :
smul_comm_class α (Π (i : I), f i) (Π (i : I), g i)
@[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)
@[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_smul (g i) (h i)] [Π (i : I), has_smul (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)
@[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)
@[protected, instance]
def pi.is_central_scalar {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_smul α (f i)] [Π (i : I), has_smul αᵐᵒᵖ (f i)] [∀ (i : I), is_central_scalar α (f i)] :
is_central_scalar α (Π (i : I), f i)
theorem pi.has_faithful_smul_at {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_smul α (f i)] [∀ (i : I), nonempty (f i)] (i : I) [has_faithful_smul α (f i)] :
has_faithful_smul α (Π (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.

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)

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

@[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)
@[protected, instance]
def pi.has_faithful_smul {I : Type u} {f : I → Type v} {α : Type u_1} [nonempty I] [Π (i : I), has_smul α (f i)] [∀ (i : I), nonempty (f i)] [∀ (i : I), has_faithful_smul α (f i)] :
has_faithful_smul α (Π (i : I), f i)
@[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
@[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
@[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
@[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
@[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
@[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
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
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.

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) :
@[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
@[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
@[protected, instance]
def function.has_vadd {ι : Type u_1} {R : Type u_2} {M : Type u_3} [has_vadd R M] :
has_vadd R (ι → M)

Non-dependent version of pi.has_vadd. Lean gets confused by the dependent instance if this is not present.

Equations
@[protected, instance]
def function.has_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [has_smul R M] :
has_smul R (ι → M)

Non-dependent version of pi.has_smul. Lean gets confused by the dependent instance if this is not present.

Equations
@[protected, instance]
def function.smul_comm_class {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [has_smul α M] [has_smul β M] [smul_comm_class α β M] :
smul_comm_class α β (ι → M)

Non-dependent version of pi.smul_comm_class. Lean gets confused by the dependent instance if this is not present.

@[protected, instance]
def function.vadd_comm_class {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [has_vadd α M] [has_vadd β M] [vadd_comm_class α β M] :
vadd_comm_class α β (ι → M)

Non-dependent version of pi.vadd_comm_class. Lean gets confused by the dependent instance if this is not present.

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₁
theorem function.update_smul {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_smul α (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₁
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₁
theorem set.piecewise_smul {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_smul α (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₁
theorem function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :
function.extend f (r g) (r e) = r function.extend f g e
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 : β → γ) :