algebra R (M →ₗ[R] M)

Stream: Is there code for X?

[Eric Wieser]

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_add' := λ _ _, add_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]

docs#module.endomorphism_algebra

[Eric Wieser]

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

[Eric Wieser]

@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]

Well obviously I prefer the naming I introduced :wink:

[Oliver Nash]

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

[Adam Topaz]

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

[Adam Topaz]

Certainly much more than "endomorphism semiring"

[Reid Barton]

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

[Eric Wieser]

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]

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

[Reid Barton]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Mario Carneiro]

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}
-- add_semigroup (with_bot ℕ)
-- inhabited (with_bot ℕ)
-- semilattice_sup_bot (with_bot ℕ)
-- add_monoid (with_bot ℕ)
-- has_well_founded (with_bot ℕ)
-- has_lt (with_bot ℕ)
-- has_to_tactic_format (with_bot ℕ)
-- lattice (with_bot ℕ)
-- has_sup (with_bot ℕ)
-- ordered_add_comm_monoid (with_bot ℕ)
-- has_to_format (with_bot ℕ)
-- has_one (with_bot ℕ)
-- distrib_lattice (with_bot ℕ)
-- preorder (with_bot ℕ)
-- add_comm_monoid (with_bot ℕ)
-- add_comm_semigroup (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 ℕ)
-- has_add (with_bot ℕ)
-- semilattice_sup (with_bot ℕ)
-- has_inf (with_bot ℕ)
-- order_bot (with_bot ℕ)
-- partial_order (with_bot ℕ)
end tactic

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/with_bot/near/196835021