Documentation

Mathlib.GroupTheory.GroupAction.Pi

Pi instances for multiplicative actions #

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

See also #

instance Pi.vadd' {I : Type u} {f : IType v} {g : IType u_1} [(i : I) → VAdd (f i) (g i)] :
VAdd ((i : I) → f i) ((i : I) → g i)
Equations
  • Pi.vadd' = { vadd := fun s x i => s i +ᵥ x i }
instance Pi.smul' {I : Type u} {f : IType v} {g : IType u_1} [(i : I) → SMul (f i) (g i)] :
SMul ((i : I) → f i) ((i : I) → g i)
Equations
  • Pi.smul' = { smul := fun s x i => s i x i }
@[simp]
theorem Pi.vadd_apply' {I : Type u} {f : IType v} (i : I) {g : IType u_1} [(i : I) → VAdd (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i) :
(((i : I) → f i) +ᵥ ((i : I) → g i)) ((i : I) → g i) instHVAdd s x i = s i +ᵥ x i
@[simp]
theorem Pi.smul_apply' {I : Type u} {f : IType v} (i : I) {g : IType u_1} [(i : I) → SMul (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i) :
(((i : I) → f i) ((i : I) → g i)) ((i : I) → g i) instHSMul s x i = s i x i
instance Pi.vaddAssocClass {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [VAdd α β] [(i : I) → VAdd β (f i)] [(i : I) → VAdd α (f i)] [∀ (i : I), VAddAssocClass α β (f i)] :
VAddAssocClass α β ((i : I) → f i)
Equations
theorem Pi.vaddAssocClass.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} {β : Type u_4} [VAdd α β] [(i : I) → VAdd β (f i)] [(i : I) → VAdd α (f i)] [∀ (i : I), VAddAssocClass α β (f i)] :
VAddAssocClass α β ((i : I) → f i)
instance Pi.isScalarTower {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [SMul α β] [(i : I) → SMul β (f i)] [(i : I) → SMul α (f i)] [∀ (i : I), IsScalarTower α β (f i)] :
IsScalarTower α β ((i : I) → f i)
Equations
theorem Pi.vaddAssocClass'.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {α : Type u_4} [(i : I) → VAdd α (f i)] [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd α (g i)] [∀ (i : I), VAddAssocClass α (f i) (g i)] :
VAddAssocClass α ((i : I) → f i) ((i : I) → g i)
instance Pi.vaddAssocClass' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [(i : I) → VAdd α (f i)] [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd α (g i)] [∀ (i : I), VAddAssocClass α (f i) (g i)] :
VAddAssocClass α ((i : I) → f i) ((i : I) → g i)
Equations
instance Pi.isScalarTower' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [(i : I) → SMul α (f i)] [(i : I) → SMul (f i) (g i)] [(i : I) → SMul α (g i)] [∀ (i : I), IsScalarTower α (f i) (g i)] :
IsScalarTower α ((i : I) → f i) ((i : I) → g i)
Equations
instance Pi.vaddAssocClass'' {I : Type u} {f : IType v} {g : IType u_1} {h : IType u_2} [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :
VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
theorem Pi.vaddAssocClass''.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {h : IType u_4} [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :
VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
instance Pi.isScalarTower'' {I : Type u} {f : IType v} {g : IType u_1} {h : IType u_2} [(i : I) → SMul (f i) (g i)] [(i : I) → SMul (g i) (h i)] [(i : I) → SMul (f i) (h i)] [∀ (i : I), IsScalarTower (f i) (g i) (h i)] :
IsScalarTower ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
theorem Pi.vaddCommClass.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} {β : Type u_4} [(i : I) → VAdd α (f i)] [(i : I) → VAdd β (f i)] [∀ (i : I), VAddCommClass α β (f i)] :
VAddCommClass α β ((i : I) → f i)
instance Pi.vaddCommClass {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [(i : I) → VAdd α (f i)] [(i : I) → VAdd β (f i)] [∀ (i : I), VAddCommClass α β (f i)] :
VAddCommClass α β ((i : I) → f i)
Equations
instance Pi.smulCommClass {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [(i : I) → SMul α (f i)] [(i : I) → SMul β (f i)] [∀ (i : I), SMulCommClass α β (f i)] :
SMulCommClass α β ((i : I) → f i)
Equations
theorem Pi.vaddCommClass'.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {α : Type u_4} [(i : I) → VAdd α (g i)] [(i : I) → VAdd (f i) (g i)] [∀ (i : I), VAddCommClass α (f i) (g i)] :
VAddCommClass α ((i : I) → f i) ((i : I) → g i)
instance Pi.vaddCommClass' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [(i : I) → VAdd α (g i)] [(i : I) → VAdd (f i) (g i)] [∀ (i : I), VAddCommClass α (f i) (g i)] :
VAddCommClass α ((i : I) → f i) ((i : I) → g i)
Equations
instance Pi.smulCommClass' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [(i : I) → SMul α (g i)] [(i : I) → SMul (f i) (g i)] [∀ (i : I), SMulCommClass α (f i) (g i)] :
SMulCommClass α ((i : I) → f i) ((i : I) → g i)
Equations
instance Pi.vaddCommClass'' {I : Type u} {f : IType v} {g : IType u_1} {h : IType u_2} [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddCommClass (f i) (g i) (h i)] :
VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
theorem Pi.vaddCommClass''.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {h : IType u_4} [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddCommClass (f i) (g i) (h i)] :
VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
instance Pi.smulCommClass'' {I : Type u} {f : IType v} {g : IType u_1} {h : IType u_2} [(i : I) → SMul (g i) (h i)] [(i : I) → SMul (f i) (h i)] [∀ (i : I), SMulCommClass (f i) (g i) (h i)] :
SMulCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
instance Pi.isCentralVAdd {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → VAdd α (f i)] [(i : I) → VAdd αᵃᵒᵖ (f i)] [∀ (i : I), IsCentralVAdd α (f i)] :
IsCentralVAdd α ((i : I) → f i)
Equations
theorem Pi.isCentralVAdd.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} [(i : I) → VAdd α (f i)] [(i : I) → VAdd αᵃᵒᵖ (f i)] [∀ (i : I), IsCentralVAdd α (f i)] :
IsCentralVAdd α ((i : I) → f i)
instance Pi.isCentralScalar {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → SMul α (f i)] [(i : I) → SMul αᵐᵒᵖ (f i)] [∀ (i : I), IsCentralScalar α (f i)] :
IsCentralScalar α ((i : I) → f i)
Equations
theorem Pi.faithfulVAdd_at {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] (i : I) [FaithfulVAdd α (f i)] :
FaithfulVAdd α ((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

theorem Pi.faithfulSMul_at {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → SMul α (f i)] [∀ (i : I), Nonempty (f i)] (i : I) [FaithfulSMul α (f i)] :
FaithfulSMul α ((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.

instance Pi.faithfulVAdd {I : Type u} {f : IType v} {α : Type u_1} [Nonempty I] [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulVAdd α (f i)] :
FaithfulVAdd α ((i : I) → f i)
Equations
theorem Pi.faithfulVAdd.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} [Nonempty I] [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulVAdd α (f i)] :
FaithfulVAdd α ((i : I) → f i)
abbrev Pi.faithfulVAdd.match_1 {I : Type u_1} (motive : Nonempty IProp) :
(x : Nonempty I) → ((i : I) → motive (_ : Nonempty I)) → motive x
Equations
Instances For
    instance Pi.faithfulSMul {I : Type u} {f : IType v} {α : Type u_1} [Nonempty I] [(i : I) → SMul α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulSMul α (f i)] :
    FaithfulSMul α ((i : I) → f i)
    Equations
    theorem Pi.addAction.proof_2 {I : Type u_1} {f : IType u_2} (α : Type u_3) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :
    ∀ (x x_1 : α) (x_2 : (i : I) → f i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
    instance Pi.addAction {I : Type u} {f : IType v} (α : Type u_1) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :
    AddAction α ((i : I) → f i)
    Equations
    theorem Pi.addAction.proof_1 {I : Type u_1} {f : IType u_2} (α : Type u_3) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :
    ∀ (x : (i : I) → f i), 0 +ᵥ x = x
    instance Pi.mulAction {I : Type u} {f : IType v} (α : Type u_1) {m : Monoid α} [(i : I) → MulAction α (f i)] :
    MulAction α ((i : I) → f i)
    Equations
    theorem Pi.addAction'.proof_2 {I : Type u_1} {f : IType u_3} {g : IType u_2} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :
    ∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
    instance Pi.addAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :
    AddAction ((i : I) → f i) ((i : I) → g i)
    Equations
    • Pi.addAction' = AddAction.mk (_ : ∀ (x : (i : I) → g i), 0 +ᵥ x = x) (_ : ∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2))
    theorem Pi.addAction'.proof_1 {I : Type u_1} {f : IType u_3} {g : IType u_2} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :
    ∀ (x : (i : I) → g i), 0 +ᵥ x = x
    instance Pi.mulAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → Monoid (f i)} [(i : I) → MulAction (f i) (g i)] :
    MulAction ((i : I) → f i) ((i : I) → g i)
    Equations
    • Pi.mulAction' = MulAction.mk (_ : ∀ (x : (i : I) → g i), 1 x = x) (_ : ∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), (x * x_1) x_2 = x x_1 x_2)
    instance Pi.smulZeroClass {I : Type u} {f : IType v} (α : Type u_1) {n : (i : I) → Zero (f i)} [(i : I) → SMulZeroClass α (f i)] :
    SMulZeroClass α ((i : I) → f i)
    Equations
    instance Pi.smulZeroClass' {I : Type u} {f : IType v} {g : IType u_1} {n : (i : I) → Zero (g i)} [(i : I) → SMulZeroClass (f i) (g i)] :
    SMulZeroClass ((i : I) → f i) ((i : I) → g i)
    Equations
    instance Pi.distribSMul {I : Type u} {f : IType v} (α : Type u_1) {n : (i : I) → AddZeroClass (f i)} [(i : I) → DistribSMul α (f i)] :
    DistribSMul α ((i : I) → f i)
    Equations
    instance Pi.distribSMul' {I : Type u} {f : IType v} {g : IType u_1} {n : (i : I) → AddZeroClass (g i)} [(i : I) → DistribSMul (f i) (g i)] :
    DistribSMul ((i : I) → f i) ((i : I) → g i)
    Equations
    instance Pi.distribMulAction {I : Type u} {f : IType v} (α : Type u_1) {m : Monoid α} {n : (i : I) → AddMonoid (f i)} [(i : I) → DistribMulAction α (f i)] :
    DistribMulAction α ((i : I) → f i)
    Equations
    • One or more equations did not get rendered due to their size.
    instance Pi.distribMulAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → Monoid (f i)} {n : (i : I) → AddMonoid (g i)} [(i : I) → DistribMulAction (f i) (g i)] :
    DistribMulAction ((i : I) → f i) ((i : I) → g i)
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Pi.single_smul {I : Type u} {f : IType v} {α : Type u_1} [Monoid α] [(i : I) → AddMonoid (f i)] [(i : I) → DistribMulAction α (f i)] [DecidableEq 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 α] [AddMonoid β] [DistribMulAction α β] [DecidableEq 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 where Lean fails to apply Pi.single_smul.

    theorem Pi.single_smul₀ {I : Type u} {f : IType v} {g : IType u_1} [(i : I) → MonoidWithZero (f i)] [(i : I) → AddMonoid (g i)] [(i : I) → DistribMulAction (f i) (g i)] [DecidableEq I] (i : I) (r : f i) (x : g i) :
    instance Pi.mulDistribMulAction {I : Type u} {f : IType v} (α : Type u_1) {m : Monoid α} {n : (i : I) → Monoid (f i)} [(i : I) → MulDistribMulAction α (f i)] :
    MulDistribMulAction α ((i : I) → f i)
    Equations
    instance Pi.mulDistribMulAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → Monoid (f i)} {n : (i : I) → Monoid (g i)} [(i : I) → MulDistribMulAction (f i) (g i)] :
    MulDistribMulAction ((i : I) → f i) ((i : I) → g i)
    Equations
    instance Function.hasVAdd {ι : Type u_1} {R : Type u_2} {M : Type u_3} [VAdd R M] :
    VAdd R (ι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} {R : Type u_2} {M : Type u_3} [SMul R M] :
    SMul R (ιM)

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

    Equations
    • Function.hasSMul = Pi.instSMul
    theorem Function.vaddCommClass.proof_1 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [VAdd α M] [VAdd β M] [VAddCommClass α β M] :
    VAddCommClass α β (ιM)
    instance Function.vaddCommClass {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [VAdd α M] [VAdd β M] [VAddCommClass α β M] :
    VAddCommClass α β (ιM)

    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} {α : Type u_2} {β : Type u_3} {M : Type u_4} [SMul α M] [SMul β M] [SMulCommClass α β M] :
    SMulCommClass α β (ιM)

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

    Equations
    theorem Function.update_vadd {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → VAdd α (f i)] [DecidableEq 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 : IType v} {α : Type u_1} [(i : I) → SMul α (f i)] [DecidableEq 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 : IType v} {α : Type u_1} [(i : I) → VAdd α (f i)] (s : Set I) [(i : I) → Decidable (i s)] (c : α) (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :
    Set.piecewise s (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ Set.piecewise s f₁ g₁
    theorem Set.piecewise_smul {I : Type u} {f : IType v} {α : Type u_1} [(i : I) → SMul α (f i)] (s : Set I) [(i : I) → Decidable (i s)] (c : α) (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :
    Set.piecewise s (c f₁) (c g₁) = c Set.piecewise s f₁ g₁
    theorem Function.extend_vadd {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd R γ] (r : R) (f : αβ) (g : αγ) (e : βγ) :
    theorem Function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul R γ] (r : R) (f : αβ) (g : αγ) (e : βγ) :
    Function.extend f (r g) (r e) = r Function.extend f g e