Using classes of linear_map

Stream: maths

[Antoine Chambert-Loir]

mathlib recommends using classes of linear maps, whenever possible, but I didn't find the function that gives me the actual linear_map when I need it.
Something like below. I also wonder why I need to explicitly type the output of lmc_to_linear_map.

import algebra.module.linear_map

variables {R : Type*} [semiring R]
variables {β γ : Type*}
  [add_comm_monoid β] [module R β]
  [add_comm_monoid γ] [module R γ]
  {F : Type*} [linear_map_class F R β γ]

def lmc_to_linear_map (h : F) : β →ₗ[R] γ :=  ⟨h, map_add _, map_smulₛₗ _⟩

example (h : F) (b : β): (lmc_to_linear_map h : β →ₗ[R] γ) b = h b := rfl

[Yakov Pechersky]

For what would you need the explicit linear map? It seems to me that you might be using the forgetful functor early. I could imagine some lemmas are too specialized to explicit linear maps, as opposed to classes. Or some constructions, like composition, require a term of the specific type.

[Antoine Chambert-Loir]

I need to define linear maps from direct sums to direct sums, but direct_sum.to_module doesn't work with classes.
Maybe I should just redefine direct_sum.to_module but those who are porting mathlib to Lean4 will object, and I understand them.

[Eric Wieser]

The function should just be coe, but maybe we didn't implement it for linear maps

[Eric Wieser]

The analogue certainly exists for additive maps

[Antoine Chambert-Loir]

coe is polytyped? it can be used to give an add_monoid_hom or a function, or whatever it has to (if the function has been provided?)

[Eric Wieser]

You have to tell it the type you expect

[Antoine Chambert-Loir]

That seems to work as I expect!

import algebra.module.linear_map

variables {R : Type*} [semiring R]
variables {β γ : Type*}
  [add_comm_monoid β] [module R β]
  [add_comm_monoid γ] [module R γ]
  {F : Type*} [linear_map_class F R β γ]

instance : has_coe F (β →ₗ[R] γ) := { coe := λ h, ⟨h, map_add h, map_smulₛₗ h⟩ }

example (h : F) (b : β): (h : β →ₗ[R] γ) b = h b :=rfl

[Eric Wieser]

I suspect you are expected to use has_coe_t; you should try and find the existing additive instance and copy the approach there

[Eric Wieser]

Notably you'll want to add the silly lemmas that a linear map coerced to itself is just itself, and that alg_hom.to_linear_map and continuous_linear_map.to_linear_map and linear_equiv.to_linear_map is the same as this coercion