Pi instances for multiplicative actions

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

See also

• GroupTheory.GroupAction.option
• GroupTheory.GroupAction.prod
• GroupTheory.GroupAction.sigma
• GroupTheory.GroupAction.sum

instance Pi.vadd' {I : Type u} {f : I → Type v} {g : I → Type u_1} [(i : I) → VAdd (f i) (g i)] : VAdd ((i : I) → f i) ((i : I) → g i)

Equations

• Pi.vadd' = { vadd := fun (s : (i : I) → f i) (x : (i : I) → g i) (i : I) => s i +ᵥ x i }

instance Pi.smul' {I : Type u} {f : I → Type v} {g : I → Type u_1} [(i : I) → SMul (f i) (g i)] : SMul ((i : I) → f i) ((i : I) → g i)

Equations

• Pi.smul' = { smul := fun (s : (i : I) → f i) (x : (i : I) → g i) (i : I) => s i • x i }

@[simp]

theorem Pi.vadd_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [(i : I) → 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) → SMul (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i) : (s • x) i = s i • x i

instance Pi.vaddAssocClass {I : Type u} {f : I → Type 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

• ⋯ = ⋯

instance Pi.isScalarTower {I : Type u} {f : I → Type 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

• ⋯ = ⋯

instance Pi.vaddAssocClass' {I : Type u} {f : I → Type v} {g : I → Type 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 : I → Type v} {g : I → Type 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 : I → Type v} {g : I → Type u_1} {h : I → Type 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

• ⋯ = ⋯

instance Pi.isScalarTower'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type 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

• ⋯ = ⋯

instance Pi.vaddCommClass {I : Type u} {f : I → Type 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 : I → Type 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

• ⋯ = ⋯

instance Pi.vaddCommClass' {I : Type u} {f : I → Type v} {g : I → Type 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 : I → Type v} {g : I → Type 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 : I → Type v} {g : I → Type u_1} {h : I → Type 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

• ⋯ = ⋯

instance Pi.smulCommClass'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type 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 : I → Type 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

• ⋯ = ⋯

instance Pi.isCentralScalar {I : Type u} {f : I → Type 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 : I → Type 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 : I → Type 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.

abbrev Pi.faithfulVAdd.match_1 {I : Type u_1} (motive : Nonempty I → Prop) : ∀ (x : Nonempty I), (∀ (i : I), motive ⋯) → motive x

Equations

• ⋯ = ⋯

instance Pi.faithfulVAdd {I : Type u} {f : I → Type 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

• ⋯ = ⋯

instance Pi.faithfulSMul {I : Type u} {f : I → Type 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

• ⋯ = ⋯

instance Pi.addAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : AddMonoid α} [(i : I) → AddAction α (f i)] : AddAction α ((i : I) → f i)

Equations

• Pi.addAction α = AddAction.mk ⋯ ⋯

theorem Pi.addAction.proof_2 {I : Type u_1} {f : I → Type 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)

theorem Pi.addAction.proof_1 {I : Type u_1} {f : I → Type 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 : I → Type v} (α : Type u_1) {m : Monoid α} [(i : I) → MulAction α (f i)] : MulAction α ((i : I) → f i)

Equations

• Pi.mulAction α = MulAction.mk ⋯ ⋯

instance Pi.addAction' {I : Type u} {f : I → Type v} {g : I → Type 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 ⋯ ⋯

theorem Pi.addAction'.proof_1 {I : Type u_1} {f : I → Type u_3} {g : I → Type u_2} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] : ∀ (x : (i : I) → g i), 0 +ᵥ x = x

theorem Pi.addAction'.proof_2 {I : Type u_1} {f : I → Type u_3} {g : I → Type 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.mulAction' {I : Type u} {f : I → Type v} {g : I → Type 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 ⋯ ⋯

instance Pi.smulZeroClass {I : Type u} {f : I → Type v} (α : Type u_1) {n : (i : I) → Zero (f i)} [(i : I) → SMulZeroClass α (f i)] : SMulZeroClass α ((i : I) → f i)

Equations

• Pi.smulZeroClass α = SMulZeroClass.mk ⋯

instance Pi.smulZeroClass' {I : Type u} {f : I → Type v} {g : I → Type 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

• Pi.smulZeroClass' = SMulZeroClass.mk ⋯

instance Pi.distribSMul {I : Type u} {f : I → Type v} (α : Type u_1) {n : (i : I) → AddZeroClass (f i)} [(i : I) → DistribSMul α (f i)] : DistribSMul α ((i : I) → f i)

Equations

• Pi.distribSMul α = DistribSMul.mk ⋯

instance Pi.distribSMul' {I : Type u} {f : I → Type v} {g : I → Type 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

• Pi.distribSMul' = DistribSMul.mk ⋯

instance Pi.distribMulAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : Monoid α} {n : (i : I) → AddMonoid (f i)} [(i : I) → DistribMulAction α (f i)] : DistribMulAction α ((i : I) → f i)

Equations

• Pi.distribMulAction α = let __src := Pi.mulAction α; let __src_1 := Pi.distribSMul α; DistribMulAction.mk ⋯ ⋯

instance Pi.distribMulAction' {I : Type u} {f : I → Type v} {g : I → Type 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

• Pi.distribMulAction' = let __src := Pi.mulAction'; let __src_1 := Pi.distribSMul'; DistribMulAction.mk ⋯ ⋯

theorem Pi.single_smul {I : Type u} {f : I → Type 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 : I → Type v} {g : I → Type 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) : Pi.single i (r • x) = Pi.single i r • Pi.single i x

instance Pi.mulDistribMulAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : Monoid α} {n : (i : I) → Monoid (f i)} [(i : I) → MulDistribMulAction α (f i)] : MulDistribMulAction α ((i : I) → f i)

Equations

• Pi.mulDistribMulAction α = let __src := Pi.mulAction α; MulDistribMulAction.mk ⋯ ⋯

instance Pi.mulDistribMulAction' {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) → MulDistribMulAction (f i) (g i)] : MulDistribMulAction ((i : I) → f i) ((i : I) → g i)

Equations

• Pi.mulDistribMulAction' = MulDistribMulAction.mk ⋯ ⋯

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

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 : I → Type 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 : I → Type 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 : I → Type 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 : I → Type 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 : β → γ) : Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend 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