## Stream: maths

### Topic: ideal v vector space

#### 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?

#### Kevin Buzzard (Jul 15 2020 at 08:34):

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

#### 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

#### Sebastien Gouezel (Jul 15 2020 at 15:52):

With an abbreviation you can do delta smooth.

#### Nicolò Cavalleri (Jul 15 2020 at 16:17):

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

#### 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.

#### 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?

#### 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


#### Mario Carneiro (Jul 16 2020 at 09:12):

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

#### 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

#### 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

#### Anne Baanen (Jul 16 2020 at 09:16):

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

#### Mario Carneiro (Jul 16 2020 at 09:16):

I thought the plan was to delete it?

#### 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.

#### 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.

#### 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?

#### 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)

#### Mario Carneiro (Jul 16 2020 at 09:23):

The story is pretty similar with vector_space

#### 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

#### 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?

#### 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

#### 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

#### 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?

#### Mario Carneiro (Jul 16 2020 at 09:33):

no, because the ring comes separately anyway

#### Mario Carneiro (Jul 16 2020 at 09:33):

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

I see

#### Utensil Song (Jul 16 2020 at 09:41):

This solves the technical problem but leaves the cognitive problem.

#### Utensil Song (Jul 16 2020 at 09:42):

@[reducible] def also can't be extended

extended?

#### 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