Module instances for FunLike types

In this file we define various instances related to modules for FunLike types.

Note that currently, these are not registered as instances, but only abbrevs to avoid long typeclass searches.

TODO:

Add definitions and API for the coercion being a linear map, similar to FunLike.coeMonoidHom, and related definitions.

theorem FunLike.isScalarTower {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M β] [SMul M' β] [SMul M F] [SMul M' F] [IsSMulApply M F α β] [IsSMulApply M' F α β] [SMul M M'] [IsScalarTower M M' β] : IsScalarTower M M' F

theorem FunLike.smulCommClass {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M β] [SMul M' β] [SMul M F] [SMul M' F] [IsSMulApply M F α β] [IsSMulApply M' F α β] [SMulCommClass M M' β] : SMulCommClass M M' F

theorem FunLike.isCentralScalar {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M F] [SMul Mᵐᵒᵖ F] [SMul M β] [SMul Mᵐᵒᵖ β] [IsCentralScalar M β] [IsSMulApply M F α β] [IsSMulApply Mᵐᵒᵖ F α β] : IsCentralScalar M F

@[reducible, inline]

abbrev FunLike.distribSMul {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [AddZeroClass β] [AddZeroClass F] [DistribSMul M β] [SMul M F] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply M F α β] : DistribSMul M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x and 0 x = 0, (f + g) x = f x + g x is a DistribSMul if β is a DistribSMul.

Equations

• FunLike.distribSMul = Function.Injective.distribSMul (FunLike.coeAddMonoidHom F α β) ⋯ ⋯

@[reducible, inline]

abbrev FunLike.mulAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [SMul M F] [Monoid M] [MulAction M β] [IsSMulApply M F α β] : MulAction M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x is a MulAction if β is a MulAction.

Equations

• FunLike.mulAction = Function.Injective.mulAction (fun (f : F) => ⇑f) ⋯ ⋯

@[reducible, inline]

abbrev FunLike.addAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [VAdd M F] [AddMonoid M] [AddAction M β] [IsVAddApply M F α β] : AddAction M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x is an AddAction if β is an AddAction.

Equations

• FunLike.addAction = Function.Injective.addAction (fun (f : F) => ⇑f) ⋯ ⋯

@[reducible, inline]

abbrev FunLike.distribMulAction {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [Monoid M] [AddMonoid β] [AddMonoid F] [DistribMulAction M β] [SMul M F] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply M F α β] : DistribMulAction M F

A FunLike type with scalar multiplication that satisfies (m • f) x = m • f x, 0 x = 0, (f + g) x = f x + g x is a DistribMulAction if β is a DistribMulAction.

Equations

• FunLike.distribMulAction = Function.Injective.distribMulAction (FunLike.coeAddMonoidHom F α β) ⋯ ⋯

@[reducible, inline]

abbrev FunLike.module {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [Semiring M] [AddCommMonoid β] [Module M β] [AddCommMonoid F] [SMul M F] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply M F α β] : Module M F

A FunLike type is a Module if β is a Module.

Equations

• FunLike.module = Function.Injective.module M (FunLike.coeAddMonoidHom F α β) ⋯ ⋯