Zulip Chat Archive

Stream: maths

Topic: ideal v vector space


view this post on Zulip Kevin Buzzard (Jul 15 2020 at 08:33):

ideal is a reducible def...

@[reducible] def ideal (R : Type u) [comm_ring R] := submodule R R

and vector_space is an abbreviation.

abbreviation vector_space (R : Type u) (M : Type v) [field R] [add_comm_group M] :=
semimodule R M

Is there any reason why one should prefer one over the other?

view this post on Zulip Kevin Buzzard (Jul 15 2020 at 08:34):

PS I'm learning a lot from rewriting the algebra hierarchy from scratch :-)

view this post on Zulip NicolΓ² Cavalleri (Jul 15 2020 at 15:46):

unfold works with def but not with abbreviation:

import geometry.manifold.times_cont_mdiff

variables {π•œ : Type*} [nondiscrete_normed_field π•œ]
{E : Type*} [normed_group E] [normed_space π•œ E]
{H : Type*} [topological_space H] (I : model_with_corners π•œ E H)
{M : Type*} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M]
{E' : Type*} [normed_group E'] [normed_space π•œ E']
{H' : Type*} [topological_space H'] (I' : model_with_corners π•œ E' H')
{M' : Type*} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M']
{f f₁ : M β†’ M'} {s s₁ t : set M} {x : M}
{m n : with_top β„•}

@[reducible] def smooth (f : M β†’ M') := times_cont_mdiff I I' ⊀ f

lemma tangent_bundle_proj_smooth : smooth I.tangent I (tangent_bundle.proj I M) :=
begin
  unfold smooth, -- error if smooth is defined with abbreviation
  rw times_cont_mdiff_iff,
  sorry,
end

If I have to be sincere I did not really understand how am I supposed to work with abbreviations in a case like this one

view this post on Zulip Sebastien Gouezel (Jul 15 2020 at 15:52):

With an abbreviation you can do delta smooth.

view this post on Zulip NicolΓ² Cavalleri (Jul 15 2020 at 16:17):

What should it be then in a situation like this one?

view this post on Zulip Sebastien Gouezel (Jul 15 2020 at 16:25):

I don't know what are the pros and cons of one and the other. To me, they are essentially equivalent.

view this post on Zulip Utensil Song (Jul 16 2020 at 09:02):

I also don't understand why vector_space is defined to be an abbreviation. https://leanprover-community.github.io/mathlib_docs/notes.html#module%20definition described pros and cons, but is sacrificing the cons the only way to gain the pros?

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:11):

I thought abbreviation would be handled before tactics, but apparently not:

import data.nat.basic

abbreviation zero : β„• := 0
notation `zero'` := 0

example {x : β„•} : x + zero = x := by rw [add_zero] {md := tactic.transparency.none} -- error, could not find `x + 0`
example {x : β„•} : x + zero' = x := by rw [add_zero] {md := tactic.transparency.none} -- success

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:12):

abbreviation is not a parsing thing, it is a kind of definition

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:13):

I guess it makes sense, because you need somewhere to hang the extra typeclass arguments that module and vector_space require

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:13):

I generally don't recommend using abbreviation at all. I haven't seen a use for it that isn't better served by another lean feature

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:16):

So we should make module a @[reducible] def?

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:16):

I thought the plan was to delete it?

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:20):

Sure, I guess they don't add much. But if that is the case, I cannot find any evidence on Zulip or in the docstrings.

view this post on Zulip Anne Baanen (Jul 16 2020 at 09:21):

Anne Baanen said:

So we should make module a @[reducible] def?

As far as I can tell (on an older version of mathlib), switching modules and vector spaces from abbreviation to @[reducible] def does not break any proofs.

view this post on Zulip Utensil Song (Jul 16 2020 at 09:22):

Mario Carneiro said:

I thought the plan was to delete it?

Why delete module? Any related discussions?

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:23):

The idea was to rename semimodule to module and delete module, which adds nothing to the structure (it is simply making one of the parameters stricter, which does not necessitate a new class)

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:23):

The story is pretty similar with vector_space

view this post on Zulip Rob Lewis (Jul 16 2020 at 09:24):

I think the most recent discussion on this was here https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Semialgebra

view this post on Zulip Utensil Song (Jul 16 2020 at 09:27):

Mario Carneiro said:

The story is pretty similar with vector_space

I get the story for module but not how it applies to vector_space. Which to rename and which to delete?

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:30):

I mean that semimodule, module, and vector_space are three names for the same data. The only difference is whether the scalar ring is a semiring, ring, or field

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:33):

I think that @[reducible] def is better than abbreviation, but I know few good applications. One famous use of @[reducible] def is ge and this is almost completely banned in mathlib because the veneer is not perfectly transparent

view this post on Zulip Utensil Song (Jul 16 2020 at 09:33):

Yes, but don't we need to refer by different names to distinguish the different constraints on the scalar ring?

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:33):

no, because the ring comes separately anyway

view this post on Zulip Mario Carneiro (Jul 16 2020 at 09:33):

you write [ring R] [add_comm_group V] [module R V]

view this post on Zulip Utensil Song (Jul 16 2020 at 09:33):

I see

view this post on Zulip Utensil Song (Jul 16 2020 at 09:41):

This solves the technical problem but leaves the cognitive problem.

view this post on Zulip Utensil Song (Jul 16 2020 at 09:42):

@[reducible] def also can't be extended

view this post on Zulip Mario Carneiro (Jul 16 2020 at 10:03):

extended?

view this post on Zulip Utensil Song (Jul 16 2020 at 12:08):

A cosmetic disadvantage is that one can not extend vector spaces as such, in definitions such as normed_space. The solution is to extend semimodule instead.


Last updated: May 06 2021 at 18:20 UTC