ideal v vector space

Stream: maths

[Kevin Buzzard]

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]

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

[Nicolò Cavalleri]

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]

With an abbreviation you can do delta smooth.

[Nicolò Cavalleri]

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

[Sebastien Gouezel]

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

[Utensil Song]

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]

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]

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

[Anne Baanen]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

I thought the plan was to delete it?

[Anne Baanen]

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]

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]

Mario Carneiro said:

I thought the plan was to delete it?

Why delete module? Any related discussions?

[Mario Carneiro]

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]

The story is pretty similar with vector_space

[Rob Lewis]

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

[Utensil Song]

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]

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]

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]

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

[Mario Carneiro]

no, because the ring comes separately anyway

[Mario Carneiro]

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

[Utensil Song]

I see

[Utensil Song]

This solves the technical problem but leaves the cognitive problem.

[Utensil Song]

@[reducible] def also can't be extended

[Mario Carneiro]

extended?

[Utensil Song]

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.