vector spaces

Stream: general

[Johan Commelin]

Before we go on a rampage proving things about vector spaces: there was some suggestion that we should just turn vector_space into notation/abbreviation for module. Maybe now is a good point to decide on this, since Kenny is already PR'ing stuff where he needs new instances of vector_space.

[Mario Carneiro]

this is also affected by my upcoming refactoring. Note that semimodule and module are also related in a similar way to module and vector_space, that is, there are no new axioms, just the parameters change.

[Johan Commelin]

Ok, so why don't we just call everything a module, and only require the base thingy to be a semiring?

[Mario Carneiro]

I'm on board with that if the rest of you are, but mathematicians seem to be picky about names

[Johan Commelin]

True, but usually we are ok with generalising a notion.

[Kenny Lau]

@Mario Carneiro why are 0 and 1 defined using ulift empty and ulift unit, instead of pempty and punit?

[Kenny Lau]

instance : has_zero cardinal.{u} := ⟨⟦ulift empty⟧⟩
instance : has_one cardinal.{u} := ⟨⟦ulift unit⟧⟩

[Mario Carneiro]

because they didn't exist at the time

[Kenny Lau]

should I change it?

[Mario Carneiro]

if you want

[Kenny Lau]

it will certainly shorten my proofs:

@[simp] theorem mk_empty : mk empty = 0 :=
fintype_card empty

@[simp] theorem mk_pempty : mk pempty = 0 :=
fintype_card pempty

@[simp] theorem mk_empty' (α : Type u) : mk (∅ : set α) = 0 :=
quotient.sound ⟨(equiv.set.empty α).trans equiv.ulift.symm⟩

@[simp] theorem mk_plift_false : mk (plift false) = 0 :=
quotient.sound ⟨equiv.plift.trans $ equiv.false_equiv_empty.trans equiv.ulift.symm⟩

@[simp] theorem mk_unit : mk unit = 1 :=
(fintype_card unit).trans nat.cast_one

@[simp] theorem mk_punit : mk punit = 1 :=
(fintype_card punit).trans nat.cast_one

@[simp] theorem mk_singleton {α : Type u} (x : α) : mk ({x} : set α) = 1 :=
quotient.sound ⟨(equiv.set.singleton x).trans equiv.ulift.symm⟩

@[simp] theorem mk_plift_true : mk (plift true) = 1 :=
quotient.sound ⟨equiv.plift.trans $ equiv.true_equiv_unit.trans $ equiv.ulift.symm⟩

@[simp] theorem mk_bool : mk bool = 2 :=
quotient.sound ⟨equiv.bool_equiv_unit_sum_unit.trans $ equiv.sum_congr equiv.ulift.symm equiv.ulift.symm⟩

@[simp] theorem mk_Prop : mk Prop = 2 :=
(quotient.sound ⟨equiv.Prop_equiv_bool⟩ : mk Prop = mk bool).trans mk_bool

@[simp] theorem mk_option {α : Type u} : mk (option α) = mk α + 1 :=
quotient.sound ⟨(equiv.option_equiv_sum_unit α).trans $ equiv.sum_congr (equiv.refl α) equiv.ulift.symm⟩

theorem mk_eq_of_injective {α β : Type u} {f : α → β} {s : set α} (hf : injective f) : mk (f '' s) = mk s :=
quotient.sound ⟨(equiv.set.image f s hf).symm⟩

[Kenny Lau]

I think empty and pempty and false should be all definitionall equal

[Kenny Lau]

but that's just me

[Kenny Lau]

the same goes with punit and true

[Mario Carneiro]

I think that punit is defeq to unit

[Kenny Lau]

now I have to prove 6 equiv lemmas about the first one

[Kenny Lau]

right, but not to true

[Mario Carneiro]

no, they can't be

[Mario Carneiro]

they are in different universes

[Kenny Lau]

then punit should be made to sort

[Kenny Lau]

also, why can't punit.star be ()?

[Kenny Lau]

@[simp] def arrow_unit_equiv_unit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
⟨λ f, punit.star, λ u f, punit.star, λ f, by funext x; cases f x; refl, λ u, by cases u; reflexivity⟩

@[simp] def unit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
⟨λ f, f punit.star, λ a u, a, λ f, by funext x; cases x; refl, λ u, rfl⟩

@[simp] def empty_arrow_equiv_unit (α : Sort*) : (empty → α) ≃ punit.{u} :=
⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩

@[simp] def pempty_arrow_equiv_unit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩

@[simp] def false_arrow_equiv_unit (α : Sort*) : (false → α) ≃ punit.{u} :=
calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
             ... ≃ punit       : empty_arrow_equiv_unit _

[Kenny Lau]

@Mario Carneiro should I change the name of these to punit etc?

[Mario Carneiro]

yes, if it says punit it should be called punit

[Kenny Lau]

the fact that it is tagged with simp makes it hard to trace

[Kenny Lau]

let's hope for the best

[Kenny Lau]

wow there's a lot more misnamed theorems

[Kenny Lau]

also what is wrong with this proof

def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
⟨λ _, punit.star, λ _, punit.star, λ u, by cases u; refl, λ u, by cases u; reflexivity⟩

[Mario Carneiro]

nothing

[Mario Carneiro]

although there are a lot more theorems where that came from

[Mario Carneiro]

any universe polymorphic definition is going to have a theorem like that

[Kevin Buzzard]

It seems weird to have to say that J is a submodule of R instead of an ideal of R.

[Kenny Lau]

nothing

seriously, reflexivity?

[Mario Carneiro]

the asymmetry is a bit odd

[Johan Commelin]

@Kevin Buzzard I think the idea was that ideal could be notation for submodule. That way it is transparent to Lean, but we can still have our beloved terminology. Of course it means that you could start talking about ideals of a module, but you should just avoid that: Lean doesn't care, you will only confuse users.

[Kevin Buzzard]

Then do we get is_ideal.add or ideal.add etc? And is_submodule.smul is different to is_ideal.smul because it's the ring multiplication in the second case. I found myself having to unfold things explicitly, it was a bit weird

[Kevin Buzzard]

I was going to wait until all the semimodule stuff died down before making any explicit comments though. I'm using ideals a lot in the Hilbert basis proof course, but I have a lot of other stuff to worry about right now so it's slow progress

[Kevin Buzzard]

For ideals you don't need to find the instance of module R R (and indeed yesterday I couldn't find it)

[Kevin Buzzard]

(but that might be because things are currently in a state of flux)

[Kenny Lau]

@Mario Carneiro so at the current moment, how should we know that a field is a vector space over itself?

[Mario Carneiro]

there is an instance for this

[Mario Carneiro]

but if it isn't working you can also introduce it locally

[Kenny Lau]

oh ok

[Kenny Lau]

def module_equiv_lc (hs : is_basis s) : β ≃ (s →₀ α) :=

[Kenny Lau]

@Mario Carneiro should I change this to the idiomatic lc \a s?

[Mario Carneiro]

that theorem is the centerpiece of my current refactoring, so I recommend you leave it alone until I'm done

[Mario Carneiro]

anyway lc A s doesn't work because s isn't a module

[Kenny Lau]

ok...

[Kenny Lau]

you see

[Kenny Lau]

this would help my dimension stuff a lot

[Mario Carneiro]

then wait

[Kenny Lau]

alright