Composing chains of linear maps

Stream: mathlib4

[Stephan Maier]

Given chains of linear maps A ->_l B ->_l C and C ->_l D ->_l ->_l E, how can I chain them to get a chain A ->_l B ->_l D ->_l ->_l E? Thanks for a hint.

[Adam Topaz]

how do you want to write "chain" in lean?

[Stephan Maier]

Just as multilinear maps written as A ->_l[R] B ->_l[R] C. There is LinearMap.comp, there are ways to compose LinerMaps and MultiLinerMaps, but somehow I fail to find the easy way to put things together. There is bound to be one!

[Adam Topaz]

If would be better if you please provide a #mwe

[Stephan Maier]

Thanks for pointing this out. Here you go:

import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.Module.Basic

example
  {R : Type u} [CommSemiring R]
  (A : Type v) [AddCommMonoid A] [Module R A]
  (B : Type v) [AddCommMonoid B] [Module R B]
  (C : Type v) [AddCommMonoid C] [Module R C]
  (D : Type v) [AddCommMonoid D] [Module R D]
  (f : A →ₗ[R] B →ₗ[R] C) (g : C  →ₗ[R] D)
  :  A  →ₗ[R] B →ₗ[R] D := -- By forming "g ∘  f" in a suitable way

[Adam Topaz]

example
  {R : Type u} [CommSemiring R]
  (A : Type v) [AddCommMonoid A] [Module R A]
  (B : Type v) [AddCommMonoid B] [Module R B]
  (C : Type v) [AddCommMonoid C] [Module R C]
  (D : Type v) [AddCommMonoid D] [Module R D]
  (f : A →ₗ[R] B →ₗ[R] C) (g : C →ₗ[R] D) :
  A →ₗ[R] B →ₗ[R] D :=
  (LinearMap.compRight g).comp f

[Adam Topaz]

I used import Mathlib, so I'm not sure if your imports suffice.

[Stephan Maier]

Cool, thanks so much! Mathlib takes getting used to...! Great stuff.

[Adam Topaz]

In case it helps, I found the LinearMap.compRight with by exact? using g once I had already put the composition with f down.

[Stephan Maier]

Thanks, I tried it, and it finds yet another solution, which is a special API, though, tailored to the purpose: LinearMap.compr₂ f g