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} [inst : (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} [inst : (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} [inst : (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} [inst : (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
def Pi.vaddAssocClass.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd α β] [inst : (i : I) → VAdd β (f i)] [inst : (i : I) → VAdd α (f i)] [inst : ∀ (i : I), VAddAssocClass α β (f i)] :
VAddAssocClass α β ((i : I) → f i)
Equations
instance Pi.vaddAssocClass {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst : (i : I) → VAdd β (f i)] [inst : (i : I) → VAdd α (f i)] [inst : ∀ (i : I), VAddAssocClass α β (f i)] :
VAddAssocClass α β ((i : I) → f i)
Equations
instance Pi.isScalarTower {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst : (i : I) → SMul β (f i)] [inst : (i : I) → SMul α (f i)] [inst : ∀ (i : I), IsScalarTower α β (f i)] :
IsScalarTower α β ((i : I) → f i)
Equations
instance Pi.vaddAssocClass' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd (f i) (g i)] [inst : (i : I) → VAdd α (g i)] [inst : ∀ (i : I), VAddAssocClass α (f i) (g i)] :
VAddAssocClass α ((i : I) → f i) ((i : I) → g i)
Equations
def Pi.vaddAssocClass'.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {α : Type u_4} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd (f i) (g i)] [inst : (i : I) → VAdd α (g i)] [inst : ∀ (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} [inst : (i : I) → SMul α (f i)] [inst : (i : I) → SMul (f i) (g i)] [inst : (i : I) → SMul α (g i)] [inst : ∀ (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} [inst : (i : I) → VAdd (f i) (g i)] [inst : (i : I) → VAdd (g i) (h i)] [inst : (i : I) → VAdd (f i) (h i)] [inst : ∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :
VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
def Pi.vaddAssocClass''.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {h : IType u_4} [inst : (i : I) → VAdd (f i) (g i)] [inst : (i : I) → VAdd (g i) (h i)] [inst : (i : I) → VAdd (f i) (h i)] [inst : ∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :
VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
  • (_ : VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : 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} [inst : (i : I) → SMul (f i) (g i)] [inst : (i : I) → SMul (g i) (h i)] [inst : (i : I) → SMul (f i) (h i)] [inst : ∀ (i : I), IsScalarTower (f i) (g i) (h i)] :
IsScalarTower ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
def Pi.vaddCommClass.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} {β : Type u_4} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd β (f i)] [inst : ∀ (i : I), VAddCommClass α β (f i)] :
VAddCommClass α β ((i : I) → f i)
Equations
instance Pi.vaddCommClass {I : Type u} {f : IType v} {α : Type u_1} {β : Type u_2} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd β (f i)] [inst : ∀ (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} [inst : (i : I) → SMul α (f i)] [inst : (i : I) → SMul β (f i)] [inst : ∀ (i : I), SMulCommClass α β (f i)] :
SMulCommClass α β ((i : I) → f i)
Equations
def Pi.vaddCommClass'.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {α : Type u_4} [inst : (i : I) → VAdd α (g i)] [inst : (i : I) → VAdd (f i) (g i)] [inst : ∀ (i : I), VAddCommClass α (f i) (g i)] :
VAddCommClass α ((i : I) → f i) ((i : I) → g i)
Equations
instance Pi.vaddCommClass' {I : Type u} {f : IType v} {g : IType u_1} {α : Type u_2} [inst : (i : I) → VAdd α (g i)] [inst : (i : I) → VAdd (f i) (g i)] [inst : ∀ (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} [inst : (i : I) → SMul α (g i)] [inst : (i : I) → SMul (f i) (g i)] [inst : ∀ (i : I), SMulCommClass α (f i) (g i)] :
SMulCommClass α ((i : I) → f i) ((i : I) → g i)
Equations
def Pi.vaddCommClass''.proof_1 {I : Type u_1} {f : IType u_2} {g : IType u_3} {h : IType u_4} [inst : (i : I) → VAdd (g i) (h i)] [inst : (i : I) → VAdd (f i) (h i)] [inst : ∀ (i : I), VAddCommClass (f i) (g i) (h i)] :
VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
  • (_ : VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)) = (_ : VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i))
instance Pi.vaddCommClass'' {I : Type u} {f : IType v} {g : IType u_1} {h : IType u_2} [inst : (i : I) → VAdd (g i) (h i)] [inst : (i : I) → VAdd (f i) (h i)] [inst : ∀ (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 : IType v} {g : IType u_1} {h : IType u_2} [inst : (i : I) → SMul (g i) (h i)] [inst : (i : I) → SMul (f i) (h i)] [inst : ∀ (i : I), SMulCommClass (f i) (g i) (h i)] :
SMulCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)
Equations
def Pi.instIsCentralVAddForAllInstVAddAddOpposite.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd αᵃᵒᵖ (f i)] [inst : ∀ (i : I), IsCentralVAdd α (f i)] :
IsCentralVAdd α ((i : I) → f i)
Equations
instance Pi.instIsCentralVAddForAllInstVAddAddOpposite {I : Type u} {f : IType v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst : (i : I) → VAdd αᵃᵒᵖ (f i)] [inst : ∀ (i : I), IsCentralVAdd α (f i)] :
IsCentralVAdd α ((i : I) → f i)
Equations
instance Pi.instIsCentralScalarForAllInstSMulMulOpposite {I : Type u} {f : IType v} {α : Type u_1} [inst : (i : I) → SMul α (f i)] [inst : (i : I) → SMul αᵐᵒᵖ (f i)] [inst : ∀ (i : I), IsCentralScalar α (f i)] :
IsCentralScalar α ((i : I) → f i)
Equations
theorem Pi.faithfulVAdd_at {I : Type u} {f : IType v} {α : Type u_1} [inst : (i : I) → VAdd α (f i)] [inst : ∀ (i : I), Nonempty (f i)] (i : I) [inst : 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} [inst : (i : I) → SMul α (f i)] [inst : ∀ (i : I), Nonempty (f i)] (i : I) [inst : 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} [inst : Nonempty I] [inst : (i : I) → VAdd α (f i)] [inst : ∀ (i : I), Nonempty (f i)] [inst : ∀ (i : I), FaithfulVAdd α (f i)] :
FaithfulVAdd α ((i : I) → f i)
Equations
abbrev Pi.faithfulVAdd.match_1 {I : Type u_1} (motive : Nonempty IProp) :
(x : Nonempty I) → ((i : I) → motive (_ : Nonempty I)) → motive x
Equations
def Pi.faithfulVAdd.proof_1 {I : Type u_1} {f : IType u_2} {α : Type u_3} [inst : Nonempty I] [inst : (i : I) → VAdd α (f i)] [inst : ∀ (i : I), Nonempty (f i)] [inst : ∀ (i : I), FaithfulVAdd α (f i)] :
FaithfulVAdd α ((i : I) → f i)
Equations
instance Pi.faithfulSMul {I : Type u} {f : IType v} {α : Type u_1} [inst : Nonempty I] [inst : (i : I) → SMul α (f i)] [inst : ∀ (i : I), Nonempty (f i)] [inst : ∀ (i : I), FaithfulSMul α (f i)] :
FaithfulSMul α ((i : I) → f i)
Equations
instance Pi.addAction {I : Type u} {f : IType v} (α : Type u_1) {m : AddMonoid α} [inst : (i : I) → AddAction α (f i)] :
AddAction α ((i : I) → f i)
Equations
def Pi.addAction.proof_1 {I : Type u_1} {f : IType u_2} (α : Type u_3) {m : AddMonoid α} [inst : (i : I) → AddAction α (f i)] :
∀ (x : (i : I) → f i), 0 +ᵥ x = x
Equations
def Pi.addAction.proof_2 {I : Type u_1} {f : IType u_2} (α : Type u_3) {m : AddMonoid α} [inst : (i : I) → AddAction α (f i)] :
∀ (x x_1 : α) (x_2 : (i : I) → f i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
Equations
instance Pi.mulAction {I : Type u} {f : IType v} (α : Type u_1) {m : Monoid α} [inst : (i : I) → MulAction α (f i)] :
MulAction α ((i : I) → f i)
Equations
def Pi.addAction'.proof_2 {I : Type u_1} {f : IType u_3} {g : IType u_2} {m : (i : I) → AddMonoid (f i)} [inst : (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)
Equations
instance Pi.addAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → AddMonoid (f i)} [inst : (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))
def Pi.addAction'.proof_1 {I : Type u_1} {f : IType u_3} {g : IType u_2} {m : (i : I) → AddMonoid (f i)} [inst : (i : I) → AddAction (f i) (g i)] :
∀ (x : (i : I) → g i), 0 +ᵥ x = x
Equations
instance Pi.mulAction' {I : Type u} {f : IType v} {g : IType u_1} {m : (i : I) → Monoid (f i)} [inst : (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)} [inst : (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)} [inst : (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)} [inst : (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)} [inst : (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)} [inst : (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)} [inst : (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} [inst : Monoid α] [inst : (i : I) → AddMonoid (f i)] [inst : (i : I) → DistribMulAction α (f i)] [inst : 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} [inst : Monoid α] [inst : AddMonoid β] [inst : DistribMulAction α β] [inst : 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} [inst : (i : I) → MonoidWithZero (f i)] [inst : (i : I) → AddMonoid (g i)] [inst : (i : I) → DistribMulAction (f i) (g i)] [inst : 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)} [inst : (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)} [inst : (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} [inst : 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} [inst : 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} [inst : VAdd α M] [inst : VAdd β M] [inst : VAddCommClass α β M] :
VAddCommClass α β (ιM)

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

Equations
def Function.vaddCommClass.proof_1 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [inst : VAdd α M] [inst : VAdd β M] [inst : VAddCommClass α β M] :
VAddCommClass α β (ιM)
Equations
instance Function.smulCommClass {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [inst : SMul α M] [inst : SMul β M] [inst : 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} [inst : (i : I) → VAdd α (f i)] [inst : 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} [inst : (i : I) → SMul α (f i)] [inst : 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} [inst : (i : I) → VAdd α (f i)] (s : Set I) [inst : (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} [inst : (i : I) → SMul α (f i)] (s : Set I) [inst : (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} [inst : VAdd R γ] (r : R) (f : αβ) (g : αγ) (e : βγ) :
theorem Function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul R γ] (r : R) (f : αβ) (g : αγ) (e : βγ) :
Function.extend f (r g) (r e) = r Function.extend f g e