submodule.le_span

Stream: Is there code for X?

[Scott Morrison]

Where is

lemma submodule.le_span (R : Type*) [semiring R] (M : Type*) [add_comm_monoid M] [module R M]
  (w : set M) : w ≤ span R w :=
sorry

?

[Johan Commelin]

It's done for the coercion to set, and called subset_span

[Johan Commelin]

@Scott Morrison probably because \le on sets is not the simp normal form

[Scott Morrison]

Oh! I'd sort of forgotten that about simp normal form. Maybe we should change that someday?

[Kevin Buzzard]

I think that all the set notation (inter, union, subseteq, empty) should be replaced with lattice notation (inf, sup, le, bot) and mathematicians should just learn to live with it

[Eric Wieser]

Does lean let us have notation `∪` = @has_sup.sup (has_union.to_has_sup) _, and if so does the pretty printer do the right thing (after removing the original notation)

[Kevin Buzzard]

Yes that's exactly the sort of thing we should be thinking about -- vector_space as some completely transparent abbreviation for module and inter notation as just meaning inf. What I've never been clear about is then how to tell the pretty printer when to use what.

[Kevin Buzzard]

The perfect solution would be to allow vector_space as a different term to module but make it super-ultra-reducible in the sense that module rewrites will work for vector spaces and yet the pretty printer will still print modules as modules and vector spaces as vector spaces. I'm not sure this is possible though

[Kevin Buzzard]

This is why I've reluctantly come to the conclusion that sometimes mathematicians will have to lump it because educating a mathematician about inf instead of inter seems to be easier than getting lean to seamlessly conflate the two

[Johan Commelin]

The pretty printer would need to do type-class inference, right?

[Gabriel Ebner]

(Talking about ∩ as notation for ⊓.) In Lean 4 this would be easy to do.

The pretty printer would need to do type-class inference, right?

You just need to check if the typeclass instance is defeq to has_union.to_has_sup. No synthesis needed.

[Johan Commelin]

For intersection that would work. But for vector_space the pretty printer needs to figure out whether the base ring of the module is a field.

[Eric Wieser]

Notation can probably figure it out if the base ring is field.to_comm_ring.to_ring.to_semiring

[Eric Wieser]

But if you match against that, then you'll miss field.to_comm_ring.to_comm_semiring.to_semiring

[Eric Wieser]

Which I think was probably why vector_space / module caused problems in the first place, as it forced typeclass resolution to go down a path it wouldn't necessarily have chosen for semimodule

[Oliver Nash]

But couldn't we just have vector_space mean module regardless of the scalars?

[Oliver Nash]

There would be occasional surprise at this divergence from the standard practice but it might be the right compromise.

[Eric Wieser]

Are you suggesting renaming module to vector_space?

[Eric Wieser]

Because having two names for the same thing seems like it would just be confusing, especially when those two names mean different things mathematically

[Oliver Nash]

I was suggesting two names for the same thing.

[Oliver Nash]

If we felt that was too likely to be confusing, presumably we could only do this within a locale.

[Oliver Nash]

(which would not remove possibility for confusion, but might reduce it )

[Kevin Buzzard]

My impression is that right now after the vector space purge we can either have everything being a module or everything being a vector space. But thinking about it maybe that's fine, because delicate maths undergraduates who learn about vector spaces on day 1 and don't learn about modules until year 3 can just have everything as a vector space, and those that know about modules will be fine calling vector spaces modules anyway.