maybe_linear_map

Stream: general

[Eric Wieser]

I've found a bunch of cases where I want to make something a linear map, but it's only possible to do so when R is commutative - most notably, this comes up when the domain or codomain of my linear map is itself a linear map.

How bad an idea is a definition like:

structure maybe_linear_map (R : Type u) (M : Type v) (M₂ : Type w)
  [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
  extends add_monoid_hom M M₂ :=
(maybe_map_smul' : (∀ c₁ c₂ : R, c₁ * c₂ = c₂ * c₁) → ∀ (c : R) x, to_fun (c • x) = c • to_fun x)

def maybe_linear_map.to_linear_map (R : Type u) (M : Type v) (M₂ : Type w)
  [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
  (f : maybe_linear_map R M M₂) : M →ₗ[R] M₂ :=
{ to_fun := f.to_fun, map_add' := f.map_add', map_smul' := f.maybe_map_smul' mul_comm }

[Gabriel Ebner]

Couldn't you restrict R instead? (Aren't the commutative elements a subring?)

[Kevin Buzzard]

The centre (the elements that commute with all other elements) is a subring, but "commutes" is just a general predicate so doesn't cut out a subset. In your use case Eric is it true that the function commutes with the action of the centre?

[Kevin Buzzard]

I don't really understand what problem this structure is solving yet. It's nothing more than is_comm_ring R -> blah. Is the issue just that you want an is_comm_ring predicate?

[Eric Wieser]

I think docs#linear_map.applyₗ is an example of where this is relevant

[Eric Wieser]

I guess docs#linear_map.applyₗ' reveals the solution here - if you use a different R in every place that one is needed, then you don't require commutativity in R, just smul_comm_class R1 R2.