Typeclasses for FunLike and algebraic operations

In this file we provide typeclasses for the compatibility of algebraic structures and FunLike instances.

These instances encode the property that algebraic operations such as addition, subtraction, and negation are given by the pointwise operations, and moreover we provide classes for 1 acting as the identity and multiplication acting as composition.

The algebraic FunLike typeclasses provide a simp lemma of the form add_apply and a norm_cast lemma coe_add.

The following Is*Apply typeclasses are available:

• IsZeroApply, IsOneApply: 0 x = 0 and 1 x = 1, respectively
• IsOneApplyEqSelf: 1 x = x
• IsAddApply, IsMulApply: (f + g) x = f x + g x and (f * g) x = f x * g x, respectively
• IsMulApplyEqComp: (f * g) x = f (g x)
• IsSubApply, IsDivApply: (f - g) x = f x - g x and (f / g) x = f x / g x, respectively
• IsNegApply, IsInvApply: (-f) x = -(f x) and (f⁻¹) x = (f x)⁻¹, respectively
• IsVAddApply, IsSMulApply IsPowApply: (n +ᵥ f) x = n +ᵥ f x, (n • f) x = n • f x, and (f ^ n) x = (f x) ^ n, respectively
• IsNatCastApply, IsIntCastApply: (n : F) x = n • x for n : ℕ and n : ℤ, respectively

For every type that declares a FunLike instance and an Add instance, there should be generally an IsAddApply instance with the proof usually being rfl. So for instance for the continuous linear maps equipped with the uniform convergence topology, we have the instance

instance instIsAddApply [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    IsAddApply (E →SLᵤ[σ, 𝔖] F) E F where
  add_apply _ _ _ := rfl

There are a few lemmas that apply to any function space as long as they have an IsAddApply instance. Then it is now possible to define generic lemmas as follows:

section FunLike

variable {F α β : Type*} [CommMonoid β] [CommMonoid F]
  [FunLike F α β] [IsOneApply F α β] [IsMulApply F α β]

open Classical in
@[to_additive (attr := simp)]
theorem prod_apply {ι : Type*} (s : Finset ι) (f : ι → F) (x : α) :
    (∏ i ∈ s, f i) x = ∏ i ∈ s, f i x := by
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h => simp [his, h]

end FunLike

class IsZeroApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Zero β] [Zero F] : Prop

IsZeroApply F α β states for all x : α, (0 : F) x = 0.

• zero_apply (x : α) : 0 x = 0

class IsOneApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [One β] [One F] : Prop

IsOneApply F α β states for all x : α, (1 : F) x = 1.

• one_apply (x : α) : 1 x = 1

@[simp]

theorem one_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : One β} {inst✝² : One F} [self : IsOneApply F α β] (x : α) : 1 x = 1

Alias of IsOneApply.one_apply.

@[simp]

theorem zero_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Zero β} {inst✝² : Zero F} [self : IsZeroApply F α β] (x : α) : 0 x = 0

class IsOneApplyEqSelf (F : Type u_1) (α : outParam (Type u_2)) [FunLike F α α] [One F] : Prop

IsOneApplyEqSelf F α α states for all x : α, (1 : F) x = x.

• one_apply_eq_self (x : α) : 1 x = x

@[simp]

theorem one_apply_eq_self {F : Type u_1} {α : outParam (Type u_2)} {inst✝ : FunLike F α α} {inst✝¹ : One F} [self : IsOneApplyEqSelf F α] (x : α) : 1 x = x

Alias of IsOneApplyEqSelf.one_apply_eq_self.

class IsAddApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Add β] [Add F] : Prop

IsAddApply F α β states for all f g : F and x : α, (f + g) x = f x + g x.

• add_apply (f g : F) (x : α) : (f + g) x = f x + g x

class IsMulApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Mul β] [Mul F] : Prop

IsMulApply F α β states for all f g : F and x : α, (f * g) x = f x * g x.

• mul_apply (f g : F) (x : α) : (f * g) x = f x * g x

@[simp]

theorem mul_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Mul β} {inst✝² : Mul F} [self : IsMulApply F α β] (f g : F) (x : α) : (f * g) x = f x * g x

Alias of IsMulApply.mul_apply.

@[simp]

theorem add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F α β] (f g : F) (x : α) : (f + g) x = f x + g x

class IsMulApplyEqComp (F : Type u_1) (α : outParam (Type u_2)) [FunLike F α α] [Mul F] : Prop

IsMulApplyEqComp F α α states for all x : α, (f * g) x = f (g x).

• mul_apply_eq_comp (f g : F) (x : α) : (f * g) x = f (g x)

@[simp]

theorem mul_apply_eq_comp {F : Type u_1} {α : outParam (Type u_2)} {inst✝ : FunLike F α α} {inst✝¹ : Mul F} [self : IsMulApplyEqComp F α] (f g : F) (x : α) : (f * g) x = f (g x)

Alias of IsMulApplyEqComp.mul_apply_eq_comp.

class IsSubApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Sub β] [Sub F] : Prop

IsSubApply F α β states for all f g : F and x : α, (f - g) x = f x - g x.

• sub_apply (f g : F) (x : α) : (f - g) x = f x - g x

class IsDivApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Div β] [Div F] : Prop

IsDivApply F α β states for all f g : F and x : α, (f / g) x = f x / g x.

• div_apply (f g : F) (x : α) : (f / g) x = f x / g x

@[simp]

theorem div_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Div β} {inst✝² : Div F} [self : IsDivApply F α β] (f g : F) (x : α) : (f / g) x = f x / g x

Alias of IsDivApply.div_apply.

@[simp]

theorem sub_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Sub β} {inst✝² : Sub F} [self : IsSubApply F α β] (f g : F) (x : α) : (f - g) x = f x - g x

class IsNegApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Neg β] [Neg F] : Prop

IsNegApply F α β states for all f : F and x : α, (-f) x = -f x.

• neg_apply (f : F) (x : α) : (-f) x = -f x

class IsInvApply (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] [Inv β] [Inv F] : Prop

IsInvApply F α β states for all f : F and x : α, f⁻¹ x = (f x)⁻¹.

• inv_apply (f : F) (x : α) : f⁻¹ x = (f x)⁻¹

@[simp]

theorem inv_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Inv β} {inst✝² : Inv F} [self : IsInvApply F α β] (f : F) (x : α) : f⁻¹ x = (f x)⁻¹

Alias of IsInvApply.inv_apply.

@[simp]

theorem neg_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Neg β} {inst✝² : Neg F} [self : IsNegApply F α β] (f : F) (x : α) : (-f) x = -f x

class IsVAddApply (M : Type u_1) (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [FunLike F α β] [VAdd M β] [VAdd M F] : Prop

IsVAddApply M F α β states for all f : F, n : M and x : α, (n +ᵥ f) x = n +ᵥ f x.

• vadd_apply (f : F) (n : M) (x : α) : (n +ᵥ f) x = n +ᵥ f x

class IsSMulApply (M : Type u_1) (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [FunLike F α β] [SMul M β] [SMul M F] : Prop

IsSMulApply M F α β states for all f : F, n : M and x : α, (n • f) x = n • f x.

• smul_apply (f : F) (r : M) (x : α) : (r • f) x = r • f x

@[simp]

theorem smul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α) : (r • f) x = r • f x

Alias of IsSMulApply.smul_apply.

@[simp]

theorem vadd_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : VAdd M β} {inst✝² : VAdd M F} [self : IsVAddApply M F α β] (f : F) (r : M) (x : α) : (r +ᵥ f) x = r +ᵥ f x

class IsPowApply (M : Type u_1) (F : Type u_2) (α : outParam (Type u_3)) (β : outParam (Type u_4)) [FunLike F α β] [Pow β M] [Pow F M] : Prop

IsPowApply M F α β states for all f : F, n : M and x : α, (f ^ n) x = (f x) ^ n.

• pow_apply (f : F) (n : M) (x : α) : (f ^ n) x = f x ^ n

@[simp]

theorem pow_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : Pow β M} {inst✝² : Pow F M} [self : IsPowApply M F α β] (f : F) (n : M) (x : α) : (f ^ n) x = f x ^ n

Alias of IsPowApply.pow_apply.

class IsNatCastApply (F : Type u_1) (α : outParam (Type u_2)) [FunLike F α α] [NatCast F] [SMul Nat α] : Prop

IsNatCastApply F α states for all n : ℕ and x : α, (n : F) x = n • x.

• natCast_apply (n : Nat) (x : α) : ↑n x = n • x

@[simp]

theorem natCast_apply {F : Type u_1} {α : outParam (Type u_2)} {inst✝ : FunLike F α α} {inst✝¹ : NatCast F} {inst✝² : SMul Nat α} [self : IsNatCastApply F α] (n : Nat) (x : α) : ↑n x = n • x

Alias of IsNatCastApply.natCast_apply.

class IsIntCastApply (F : Type u_1) (α : outParam (Type u_2)) [FunLike F α α] [IntCast F] [SMul Int α] : Prop

IsIntCastApply F α states for all n : ℤ and x : α, (n : F) x = n • x.

• intCast_apply (n : Int) (x : α) : ↑n x = n • x

@[simp]

theorem intCast_apply {F : Type u_1} {α : outParam (Type u_2)} {inst✝ : FunLike F α α} {inst✝¹ : IntCast F} {inst✝² : SMul Int α} [self : IsIntCastApply F α] (n : Int) (x : α) : ↑n x = n • x

Alias of IsIntCastApply.intCast_apply.

theorem FunLike.coe_one {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [One F] [One β] [IsOneApply F α β] : ⇑1 = 1

theorem FunLike.coe_zero {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F α β] : ⇑0 = 0

theorem FunLike.coe_mul {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Mul F] [Mul β] [IsMulApply F α β] (f g : F) : ⇑(f * g) = ⇑f * ⇑g

theorem FunLike.coe_add {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

theorem FunLike.coe_div {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Div F] [Div β] [IsDivApply F α β] (f g : F) : ⇑(f / g) = ⇑f / ⇑g

theorem FunLike.coe_sub {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Sub F] [Sub β] [IsSubApply F α β] (f g : F) : ⇑(f - g) = ⇑f - ⇑g

theorem FunLike.coe_inv {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Inv F] [Inv β] [IsInvApply F α β] (f : F) : ⇑f⁻¹ = (⇑f)⁻¹

theorem FunLike.coe_neg {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Neg F] [Neg β] [IsNegApply F α β] (f : F) : ⇑(-f) = -⇑f

theorem FunLike.coe_smul {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F α β] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

theorem FunLike.coe_vadd {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [VAdd M F] [VAdd M β] [IsVAddApply M F α β] (n : M) (f : F) : ⇑(n +ᵥ f) = n +ᵥ ⇑f

theorem FunLike.coe_pow {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Pow F M] [Pow β M] [IsPowApply M F α β] (f : F) (n : M) : ⇑(f ^ n) = ⇑f ^ n

theorem FunLike.coe_smul' {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F α β] (f : F) (n : M) : ⇑(n • f) = n • ⇑f

theorem FunLike.coe_one_eq_id {F' : Type u_4} {α : Type u_5} [FunLike F' α α] [One F'] [IsOneApplyEqSelf F' α] : ⇑1 = id

theorem FunLike.coe_mul_eq_comp {F' : Type u_4} {α : Type u_5} [FunLike F' α α] [Mul F'] [IsMulApplyEqComp F' α] (f g : F') : ⇑(f * g) = ⇑f ∘ ⇑g

theorem FunLike.coe_natCast {F' : Type u_4} {α : Type u_5} [FunLike F' α α] [NatCast F'] [One F'] [SMul Nat α] [SMul Nat F'] [IsSMulApply Nat F' α α] [IsNatCastApply F' α] [IsOneApplyEqSelf F' α] (n : Nat) : ↑n = n • 1

theorem FunLike.coe_intCast {F' : Type u_4} {α : Type u_5} [FunLike F' α α] [IntCast F'] [One F'] [SMul Int α] [SMul Int F'] [IsSMulApply Int F' α α] [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : Int) : ↑n = n • 1