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 #

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 }
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 }
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
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
@[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
@[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
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
instance 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)
Equations
  • =
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

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.

instance 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)
Equations
  • =
instance 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)
Equations
  • =
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
theorem Pi.addAction.proof_1 {ι : Type u_1} {α : ιType u_2} (M : Type u_3) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] :
∀ (x : (i : ι) → α i), 0 +ᵥ x = x
theorem Pi.addAction.proof_2 {ι : Type u_1} {α : ιType u_2} (M : Type u_3) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] :
∀ (x x_1 : M) (x_2 : (i : ι) → α i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
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
theorem Pi.addAction'.proof_2 {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] :
∀ (x x_1 : (i : ι) → α i) (x_2 : (i : ι) → β i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
theorem Pi.addAction'.proof_1 {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] :
∀ (x : (i : ι) → β i), 0 +ᵥ x = x
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
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
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
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
instance 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.

Equations
  • =
instance 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.

Equations
  • =
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₁
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₁
theorem Function.extend_vadd {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [VAdd M β] (r : M) (f : ια) (g : ιβ) (e : αβ) :
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
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₁ : (i : ι) → α i) (g₁ : (i : ι) → α i) :
s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁
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₁ : (i : ι) → α i) (g₁ : (i : ι) → α i) :
s.piecewise (c f₁) (c g₁) = c s.piecewise f₁ g₁