Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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_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

view this post on Zulip Eric Wieser (Nov 17 2020 at 17:30):

docs#module.endomorphism_algebra

view this post on Zulip Eric Wieser (Nov 17 2020 at 17:40):

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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Nov 17 2020 at 20:27):

Well obviously I prefer the naming I introduced :wink:

view this post on Zulip Oliver Nash (Nov 17 2020 at 20:28):

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

view this post on Zulip Adam Topaz (Nov 17 2020 at 20:37):

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

view this post on Zulip Adam Topaz (Nov 17 2020 at 20:40):

Certainly much more than "endomorphism semiring"

view this post on Zulip Reid Barton (Nov 17 2020 at 20:46):

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

view this post on Zulip 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".

view this post on Zulip Reid Barton (Nov 17 2020 at 21:37):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 17 2020 at 22:20):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 00:35):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 08:31):

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

view this post on Zulip Eric Wieser (Nov 18 2020 at 08:31):

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

view this post on Zulip Reid Barton (Nov 18 2020 at 11:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 18 2020 at 12:22):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:28):

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

view this post on Zulip 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}
-- 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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 12:34):

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


Last updated: May 07 2021 at 21:10 UTC