projective space

Stream: maths

[Jakob von Raumer]

Is there a definition of the projective space $\mathcal{P}(V)$ over a vector space $V$ in mathlib that I'm missing?

[Johan Commelin]

Nope, unfortunately not yet

[Heather Macbeth]

I think @Adam Topaz has a branch.

[Adam Topaz]

branch#proj-space-quot it's very stale

[Adam Topaz]

Bah!

[Jakob von Raumer]

Thanks! I'll check it out

[Adam Topaz]

Feel free to adopt!

[Adam Topaz]

I've just been too busy with other things to work on this

[Jakob von Raumer]

I've been starting a little formalisation of (synthetic) projective geometry and it would be nice to have projective spaces as an example :)

[Johan Commelin]

@Jakob von Raumer Is your code available somewhere?

[Jakob von Raumer]

Not yet publicly, I'll post it here, when it's ready :)
I've been basing it on a collinearity relation as the only atomic judgment as in "Modern Projective Geometry" by Frölicher and Faure:

class projective_geom (G : Type u) : Type u :=
  (col : G → G → G → Prop)
  (refl13        : ∀ a b, col a b a)
  (trans_neq     : ∀ {a b p q}, p ≠ q → col a p q → col b p q → col a b p)
  (intersect_mid : ∀ {a b c d p : G}, col p a b → col p c d → {q : G // col q a c ∧ col q b d})

[Adam Topaz]

One of my long term goals is to formalize the general version of the fundamental theorem of projective geometry that appears in that book. The one that characterizes general semilinear maps in terms of partially defined maps on projective spaces

[Adam Topaz]

It would also be nice to formalize the "coordinatization" theorems for axiomatic projective spaces, which tell you when an abstract thing defined as an incidence relation actually arises from a vector space over a field (or a division algebra)

[Johan Commelin]

@Jakob von Raumer So projective_geom only models 2-dimensional projective space, is that right?

[Johan Commelin]

Or is it actually more general? I never thought about these axiomatic approaches

[Adam Topaz]

I think this works for arbitrary dimension

[Adam Topaz]

The assumptions in the third axiom essentially put you in a 2 dimensional context spanned by p a b c and d

[Jakob von Raumer]

You can add additional axioms if you want to fix a minimum or maximum dimension. I think most common is assuming the existence of a line and a point not on that line.

[Jakob von Raumer]

Working with all these coercions from K to units Kwhat's the best way to replace d by an element of units K here?

_inst_1: field K
...
d: K
h: ↑(b • v') = d • ↑(a • u')
hd: d ≠ 0
⊢ ↑v' = (d * ↑a / ↑b) • ↑u'

[Anne Baanen]

docs#units.mk0

[Anne Baanen]

In particular, I'd try something along the lines of rw ← units.coe_mk0 d hd

[Eric Wieser]

Does tactic#lift work?

[Jakob von Raumer]

Thanks, @Anne Baanen, that works.

[Jakob von Raumer]

@Eric Wieser Not yet, it seems to be lacking an instance of can_lift

Failed to find a lift from K to units K. Provide an instance of can_lift K (units K)

[Jakob von Raumer]

Eric Wieser said:

Does tactic#lift work?

Gives me

dsimplify tactic failed to simplify
state:
...
⊢ can_lift.cond (units K) d

Even though dsimp actually does reduce the above to d ≠ 0..

[Eric Wieser]

I think we should probide that instance

[Jakob von Raumer]

I did, but it still fails.

instance : can_lift K (units K) :=
⟨λ d, d, λ d, d ≠ 0, λ d hd, by { rw ← units.coe_mk0 hd, exact ⟨_, rfl⟩ }⟩

[Eric Wieser]

instance {M} [group_with_zero M] : can_lift M (units M) :=
{ coe := coe,
  cond := (≠ 0),
  prf := λ x hx, ⟨_, units.coe_mk0 hx⟩ }

(edit: #7857)

[Eric Wieser]

(sorry, cross-post)

[Eric Wieser]

Can you give a mwe?

[Jakob von Raumer]

Ah, it was some mistake in my instance. Not sure what exactly, but it works with yours.

[Eric Wieser]

Perhaps K had too strong a typeclass

[Eric Wieser]

[Jakob von Raumer]

with matlib's definition of linear independence, is it feasible to argue comfortably about (multi)sets of two or three vectors? coercing them to families over fin 2 seems unwieldy...

[Adam Topaz]

Do multisets have a coercion to type?

[Adam Topaz]

if so, you can just take the multiset itself to be the indexing type

[Yakov Pechersky]

No, but finsets do. If a multiset.to_finset is not equal to the starting multiset, then it is surely not linearly independent, because you have a duplicate.

[Yakov Pechersky]

(Although it depends on how you treat the zero vector)

[Adam Topaz]

@Jakob von Raumer do you know about matrix notation?

[Adam Topaz]

import data.matrix.notation
import linear_algebra

open_locale matrix

variables {k V : Type*} [field k] [add_comm_group V] [vector_space k V]

example {a b c : V} : ![a,b,c] 0 = a := rfl
example {a b c : V} : ![a,b,c] 1 = b := rfl
example {a b c : V} : ![a,b,c] 2 = c := rfl

[Jakob von Raumer]

Thanks for the replies, I'll start toying around with this next week. The matrix notation looks cool!

[Jakob von Raumer]

The kind of statement I'm trying to prove is along the lines of "if a, b, c are lin. dep., a, b, d are lin. dep. and c, d, are indep, then a, c, d are lin. dep.". Not sure if I should maybe check out @Peter Nelson's matroid to make this more abstract