Pi instances for multiplicative actions

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

See also

• group_theory.group_action.prod
• group_theory.group_action.sigma
• group_theory.group_action.sum

instance PiProp.hasVadd {I : Prop} {f : I → Type v} {α : Type u_1} [(i : I) → VAdd α (f i)] : VAdd α ((i : I) → f i)

Equations

• PiProp.hasVadd = { vadd := fun (s : α) (x : (i : I) → f i) (i : I) => s +ᵥ x i }

instance PiProp.hasSmul {I : Prop} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] : SMul α ((i : I) → f i)

Equations

• PiProp.hasSmul = { smul := fun (s : α) (x : (i : I) → f i) (i : I) => s • x i }

theorem PiProp.vadd_def {I : Prop} {f : I → Type v} (x : (i : I) → f i) {α : Type u_1} [(i : I) → VAdd α (f i)] (s : α) : s +ᵥ x = fun (i : I) => s +ᵥ x i

theorem PiProp.smul_def {I : Prop} {f : I → Type v} (x : (i : I) → f i) {α : Type u_1} [(i : I) → SMul α (f i)] (s : α) : s • x = fun (i : I) => s • x i

@[simp]

theorem PiProp.vadd_apply {I : Prop} {f : I → Type v} (x : (i : I) → f i) (i : I) {α : Type u_1} [(i : I) → VAdd α (f i)] (s : α) : (s +ᵥ x) i = s +ᵥ x i

@[simp]

theorem PiProp.smul_apply {I : Prop} {f : I → Type v} (x : (i : I) → f i) (i : I) {α : Type u_1} [(i : I) → SMul α (f i)] (s : α) : (s • x) i = s • x i

instance PiProp.hasVadd' {I : Prop} {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

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

instance PiProp.hasSmul' {I : Prop} {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

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

@[simp]

theorem PiProp.vadd_apply' {I : Prop} {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 PiProp.smul_apply' {I : Prop} {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 PiProp.isScalarTower {I : Prop} {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 PiProp.is_scalar_tower' {I : Prop} {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 PiProp.is_scalar_tower'' {I : Prop} {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 PiProp.sAddCommClass {I : Prop} {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 PiProp.sMulCommClass {I : Prop} {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 PiProp.vadd_comm_class' {I : Prop} {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 PiProp.smul_comm_class' {I : Prop} {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 PiProp.vadd_comm_class'' {I : Prop} {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 PiProp.smul_comm_class'' {I : Prop} {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 PiProp.instIsCentralScalarForall_conNF {I : Prop} {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 PiProp.has_faithful_vadd_at {I : Prop} {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)

theorem PiProp.faithfulSMul_at {I : Prop} {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.

instance PiProp.has_faithful_vadd {I : Prop} {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

• ⋯ = ⋯

abbrev PiProp.has_faithful_vadd.match_1 {I : Prop} (motive : Nonempty I → Prop) : ∀ (x : Nonempty I), (∀ (i : I), motive ⋯) → motive x

Equations

• ⋯ = ⋯

instance PiProp.faithfulSMul {I : Prop} {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

• ⋯ = ⋯

theorem PiProp.addAction.proof_2 {I : Prop} {f : I → Type u_1} (α : Type u_2) {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 PiProp.addAction.proof_1 {I : Prop} {f : I → Type u_1} (α : Type u_2) {m : AddMonoid α} [(i : I) → AddAction α (f i)] : ∀ (x : (i : I) → f i), 0 +ᵥ x = x

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

Equations

• PiProp.addAction α = AddAction.mk ⋯ ⋯

instance PiProp.mulAction {I : Prop} {f : I → Type v} (α : Type u_1) {m : Monoid α} [(i : I) → MulAction α (f i)] : MulAction α ((i : I) → f i)

Equations

• PiProp.mulAction α = MulAction.mk ⋯ ⋯

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

instance PiProp.addAction' {I : Prop} {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

• PiProp.addAction' = AddAction.mk ⋯ ⋯

theorem PiProp.addAction'.proof_2 {I : Prop} {f : I → Type u_2} {g : I → Type u_1} {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 PiProp.mulAction' {I : Prop} {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

• PiProp.mulAction' = MulAction.mk ⋯ ⋯

instance PiProp.distribMulAction {I : Prop} {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

• PiProp.distribMulAction α = let __src := PiProp.mulAction α; DistribMulAction.mk ⋯ ⋯

instance PiProp.distribMulAction' {I : Prop} {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

• PiProp.distribMulAction' = DistribMulAction.mk ⋯ ⋯

instance PiProp.mulDistribMulAction {I : Prop} {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

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

instance PiProp.mulDistribMulAction' {I : Prop} {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

• PiProp.mulDistribMulAction' = MulDistribMulAction.mk ⋯ ⋯

instance FunctionProp.hasVadd {ι : Prop} {R : Type u_1} {M : Type u_2} [VAdd R M] : VAdd R (ι → M)

Equations

• FunctionProp.hasVadd = PiProp.hasVadd

instance FunctionProp.hasSmul {ι : Prop} {R : Type u_1} {M : Type u_2} [SMul R M] : SMul R (ι → M)

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

Equations

• FunctionProp.hasSmul = PiProp.hasSmul

instance FunctionProp.sAddCommClass {ι : Prop} {α : Type u_1} {β : Type u_2} {M : Type u_3} [VAdd α M] [VAdd β M] [VAddCommClass α β M] : VAddCommClass α β (ι → M)

Equations

• ⋯ = ⋯

instance FunctionProp.sMulCommClass {ι : Prop} {α : Type u_1} {β : Type u_2} {M : Type u_3} [SMul α M] [SMul β M] [SMulCommClass α β M] : SMulCommClass α β (ι → M)

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

Equations

• ⋯ = ⋯