## Stream: Is there code for X?

### Topic: algebra R (M →ₗ[R] M)

#### Eric Wieser (Nov 17 2020 at 17:28):

Does this instance exist anywhere? If not, which file would it belong in?

import algebra.algebra.basic
import linear_algebra.basic

variables {M : Type*} {R : Type*} [comm_semiring R] [add_comm_monoid M] [semimodule R M]

namespace linear_map

instance : algebra R (M →ₗ[R] M) :=
{ to_fun := λ r, r • 1,
smul_def' := λ r x, by rw [algebra.smul_mul_assoc, one_mul],
map_one' := one_smul _ _,
map_zero' := zero_smul _ _,
map_mul' := λ _ _, mul_smul _ _ _,
commutes' := λ r m, by simp only [mul_one, one_mul, algebra.mul_smul_comm, algebra.smul_mul_assoc],
..linear_map.semimodule }

example (r : R) (m : M) : algebra_map R (M →ₗ[R] M) r m = r • m := rfl

end linear_map


#### Eric Wieser (Nov 17 2020 at 17:30):

docs#module.endomorphism_algebra

#### Eric Wieser (Nov 17 2020 at 17:40):

Although in my defense, the naming is inconsistent wrt docs#linear_map.endomorphism_semiring

#### Eric Wieser (Nov 17 2020 at 17:45):

@Oliver Nash, you added the algebra this way back in #1618, while the ring predates it from #456 (@Mario Carneiro) - do you have a preference between the names? It would be good to make them consistent.

#### Oliver Nash (Nov 17 2020 at 20:27):

Well obviously I prefer the naming I introduced :wink:

#### Oliver Nash (Nov 17 2020 at 20:28):

More seriously, either system seems fine and I agree we should be consistent.

#### Adam Topaz (Nov 17 2020 at 20:37):

I would say that "endomorphism algebra" is more common in the maths literature

#### Adam Topaz (Nov 17 2020 at 20:40):

Certainly much more than "endomorphism semiring"

#### Reid Barton (Nov 17 2020 at 20:46):

Normally we don't care that much about instance names anyways

#### Eric Wieser (Nov 17 2020 at 21:33):

That's a good point, instance names don't usually matter. In my case, it was a case of "I know this exists somewhere, but I don't know where to find it".

#### Reid Barton (Nov 17 2020 at 21:37):

but I'm actually not sure what inconsistency you mean, is it the namespace?

#### Reid Barton (Nov 17 2020 at 21:37):

It seems to me that endomorphism_algebra is an instance of algebra and endomorphism_semiring is an instance of semiring

#### Eric Wieser (Nov 17 2020 at 22:20):

Yes, the namespaces don't match, that was my point.

#### Mario Carneiro (Nov 18 2020 at 00:35):

I think it makes sense for these to be in the linear_map namespace

#### Eric Wieser (Nov 18 2020 at 08:31):

I guess the other name to consider consistency with here is docs#module.End

#### Eric Wieser (Nov 18 2020 at 08:31):

So perhaps module.End.semiring and module.End.algebra?

#### Reid Barton (Nov 18 2020 at 11:34):

that would suggest these are instances for End, which they are not

#### Reid Barton (Nov 18 2020 at 11:34):

I don't understand why we care about the namespaces of instances... surely it's just whatever namespace was in effect when the instance was declared

#### Reid Barton (Nov 18 2020 at 11:41):

Put differently: what's the original problem here? Is it that it can be hard to find out what instances exist for something because they could be defined anywhere (I agree)? If so then let's focus on that

#### Patrick Massot (Nov 18 2020 at 12:05):

You can still go to docs#algebra, click on instances and search there. It's a long list in this case, but not that long, and you can search for endomorphism.

#### Eric Wieser (Nov 18 2020 at 12:21):

Reid Barton said:

that would suggest these are instances for End, which they are not

Given End is an abbreviation, doesn't that mean these _are_ instances for End?

#### Reid Barton (Nov 18 2020 at 12:22):

Oh I see, the documentation doesn't show abbreviations.

#### Eric Wieser (Nov 18 2020 at 12:24):

In this particular case, the confusion came from the docstring for End indicating the presence of an instance that I couldn't find

#### Eric Wieser (Nov 18 2020 at 12:25):

But in general it's hard - if I'm looking for whether a type supports multiplication, I need to scan for semiring, distrib, monoid, ... instances - expanding has_mul is not going to help me much.

#### Mario Carneiro (Nov 18 2020 at 12:26):

I recall there was some tactic that was written (by me?) to collect all the typeclasses on a type

#### Eric Wieser (Nov 18 2020 at 12:28):

It would be great if that tactic could be executed by doc-gen

#### Mario Carneiro (Nov 18 2020 at 12:33):

I found this in my mile long test.lean file, so it is probably on zulip somewhere

import order
namespace tactic

meta def env_fold {α} (a : α) (f : declaration → α → tactic α) : tactic α :=
get_env >>= λ e s, e.fold ((return a : tactic _) s) $λ d t, interaction_monad.result.cases_on t (f d) result.exception #print interaction_monad.monad meta def get_all_classes : tactic (list name) := list.reverse <$> env_fold [] (λ d l,
mcond (is_class (expr.const d.to_name (level.param <\$> d.univ_params)))
(return (d.to_name :: l)) (return l))

meta def list_instances (e : expr) : tactic (list expr) :=
get_all_classes >>= list.mfoldr (λ n l,
(do e' ← mk_app n [e],
mk_instance e' >> return (e' :: l)) <|>
return l) [] .

open interactive interactive.types
meta def interactive.list_instances (e : parse texpr) : tactic unit :=
to_expr e >>= list_instances >>= list.mmap' trace

run_cmd list_instances (with_bot ℕ) >>= trace

example : true := by {list_instances (with_bot ℕ), trivial}
-- inhabited (with_bot ℕ)
-- semilattice_sup_bot (with_bot ℕ)
-- has_well_founded (with_bot ℕ)
-- has_lt (with_bot ℕ)
-- has_to_tactic_format (with_bot ℕ)
-- lattice (with_bot ℕ)
-- has_sup (with_bot ℕ)
-- has_to_format (with_bot ℕ)
-- has_one (with_bot ℕ)
-- distrib_lattice (with_bot ℕ)
-- preorder (with_bot ℕ)
-- has_zero (with_bot ℕ)
-- has_bot (with_bot ℕ)
-- has_sizeof (with_bot ℕ)
-- semilattice_inf (with_bot ℕ)
-- reflected (with_bot ℕ)
-- has_le (with_bot ℕ)
-- nonempty (with_bot ℕ)
-- linear_order (with_bot ℕ)
-- decidable_linear_order (with_bot ℕ)
-- semilattice_inf_bot (with_bot ℕ)
`