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.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
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
@[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
@[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
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
source
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
  • ⋯ = ⋯
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_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
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
  • ⋯ = ⋯
source
abbrev Pi.faithfulVAdd.match_1 {ι : Type u_1} (motive : Nonempty ι → Prop) :
∀ (x : Nonempty ι), (∀ (i : ι), motive ⋯) → motive x
Equations
  • ⋯ = ⋯
Instances For
    source
    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
    • ⋯ = ⋯
    source
    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
    source
    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)
    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} (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} {β : ι → Type u_5} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] :
    AddAction ((i : ι) → α i) ((i : ι) → β i)
    Equations
    source
    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)
    source
    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
    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 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
    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.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
    • ⋯ = ⋯
    source
    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
    • ⋯ = ⋯
    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.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.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 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 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₁
    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₁ : (i : ι) → α i) (g₁ : (i : ι) → α i) :
    s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁