Documentation

Mathlib.Algebra.Group.Action.Pi

Pi instances for multiplicative actions #

This file defines instances for MulAction and related structures on Pi types.

See also #

source
instance Pi.smul' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul (α i) (β i)] :
SMul ((i : ι) → α i) ((i : ι) → β i)
Equations
  • Pi.smul' = { smul := fun (s : (i : ι) → α i) (x : (i : ι) → β i) (i : ι) => s i • x i }
source
instance Pi.vadd' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd (α i) (β i)] :
VAdd ((i : ι) → α i) ((i : ι) → β i)
Equations
  • Pi.vadd' = { vadd := fun (s : (i : ι) → α i) (x : (i : ι) → β i) (i : ι) => s i +ᵥ x i }
source
theorem Pi.smul_def' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) :
s • x = fun (i : ι) => s i • x i
source
theorem Pi.vadd_def' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) :
s +ᵥ x = fun (i : ι) => s i +ᵥ x i
source
@[simp]
theorem Pi.smul_apply' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) :
(s • x) i = s i • x i
source
@[simp]
theorem Pi.vadd_apply' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) :
(s +ᵥ x) i = s i +ᵥ x i
source
theorem Pi.isScalarTower {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [SMul M N] [(i : ι) → SMul N (α i)] [(i : ι) → SMul M (α i)] [∀ (i : ι), IsScalarTower M N (α i)] :
IsScalarTower M N ((i : ι) → α i)
source
theorem Pi.vaddAssocClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [VAdd M N] [(i : ι) → VAdd N (α i)] [(i : ι) → VAdd M (α i)] [∀ (i : ι), VAddAssocClass M N (α i)] :
VAddAssocClass M N ((i : ι) → α i)
source
theorem Pi.isScalarTower' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul M (α i)] [(i : ι) → SMul (α i) (β i)] [(i : ι) → SMul M (β i)] [∀ (i : ι), IsScalarTower M (α i) (β i)] :
IsScalarTower M ((i : ι) → α i) ((i : ι) → β i)
source
theorem Pi.vaddAssocClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd (α i) (β i)] [(i : ι) → VAdd M (β i)] [∀ (i : ι), VAddAssocClass M (α i) (β i)] :
VAddAssocClass M ((i : ι) → α i) ((i : ι) → β i)
source
theorem Pi.isScalarTower'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → SMul (α i) (β i)] [(i : ι) → SMul (β i) (γ i)] [(i : ι) → SMul (α i) (γ i)] [∀ (i : ι), IsScalarTower (α i) (β i) (γ i)] :
IsScalarTower ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
source
theorem Pi.vaddAssocClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → VAdd (α i) (β i)] [(i : ι) → VAdd (β i) (γ i)] [(i : ι) → VAdd (α i) (γ i)] [∀ (i : ι), VAddAssocClass (α i) (β i) (γ i)] :
VAddAssocClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
source
theorem Pi.smulCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul N (α i)] [∀ (i : ι), SMulCommClass M N (α i)] :
SMulCommClass M N ((i : ι) → α i)
source
theorem Pi.vaddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)] :
VAddCommClass M N ((i : ι) → α i)
source
theorem Pi.smulCommClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul M (β i)] [(i : ι) → SMul (α i) (β i)] [∀ (i : ι), SMulCommClass M (α i) (β i)] :
SMulCommClass M ((i : ι) → α i) ((i : ι) → β i)
source
theorem Pi.vaddCommClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd M (β i)] [(i : ι) → VAdd (α i) (β i)] [∀ (i : ι), VAddCommClass M (α i) (β i)] :
VAddCommClass M ((i : ι) → α i) ((i : ι) → β i)
source
theorem Pi.smulCommClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → SMul (β i) (γ i)] [(i : ι) → SMul (α i) (γ i)] [∀ (i : ι), SMulCommClass (α i) (β i) (γ i)] :
SMulCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
source
theorem Pi.vaddCommClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → VAdd (β i) (γ i)] [(i : ι) → VAdd (α i) (γ i)] [∀ (i : ι), VAddCommClass (α i) (β i) (γ i)] :
VAddCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
source
theorem Pi.isCentralScalar {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul Mᵐᵒᵖ (α i)] [∀ (i : ι), IsCentralScalar M (α i)] :
IsCentralScalar M ((i : ι) → α i)
source
theorem Pi.isCentralVAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd Mᵃᵒᵖ (α i)] [∀ (i : ι), IsCentralVAdd M (α i)] :
IsCentralVAdd M ((i : ι) → α i)
source
theorem Pi.faithfulSMul_at {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] :
FaithfulSMul M ((i : ι) → α i)

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

source
theorem Pi.faithfulVAdd_at {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι) [FaithfulVAdd M (α i)] :
FaithfulVAdd M ((i : ι) → α i)

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

source
theorem Pi.faithfulSMul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [(i : ι) → SMul M (α i)] [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulSMul M (α i)] :
FaithfulSMul M ((i : ι) → α i)
source
theorem Pi.faithfulVAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [(i : ι) → VAdd M (α i)] [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulVAdd M (α i)] :
FaithfulVAdd M ((i : ι) → α i)
source
instance Pi.mulAction {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : Monoid M} [(i : ι) → MulAction M (α i)] :
MulAction M ((i : ι) → α i)
Equations
source
instance Pi.addAction {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] :
AddAction M ((i : ι) → α i)
Equations
source
instance Pi.mulAction' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → Monoid (α i)} [(i : ι) → MulAction (α i) (β i)] :
MulAction ((i : ι) → α i) ((i : ι) → β i)
Equations
source
instance Pi.addAction' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] :
AddAction ((i : ι) → α i) ((i : ι) → β i)
Equations
source
instance Function.hasSMul {ι : Type u_1} {M : Type u_2} {α : Type u_7} [SMul M α] :
SMul M (ι → α)

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

Equations
  • Function.hasSMul = Pi.instSMul
source
instance Function.hasVAdd {ι : Type u_1} {M : Type u_2} {α : Type u_7} [VAdd M α] :
VAdd M (ι → α)

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

Equations
  • Function.hasVAdd = Pi.instVAdd
source
theorem Function.smulCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass M N (ι → α)

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

source
theorem Function.vaddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M N (ι → α)

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

source
theorem Function.update_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [DecidableEq ι] (c : M) (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i) :
Function.update (c • f₁) i (c • x₁) = c • Function.update f₁ i x₁
source
theorem Function.update_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [DecidableEq ι] (c : M) (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i) :
Function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ Function.update f₁ i x₁
source
theorem Function.extend_smul {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) :
Function.extend f (r • g) (r • e) = r • Function.extend f g e
source
theorem Function.extend_vadd {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [VAdd M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) :
Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e
source
theorem Set.piecewise_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] (s : Set ι) [(i : ι) → Decidable (i ∈ s)] (c : M) (f₁ g₁ : (i : ι) → α i) :
s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁
source
theorem Set.piecewise_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] (s : Set ι) [(i : ι) → Decidable (i ∈ s)] (c : M) (f₁ g₁ : (i : ι) → α i) :
s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁