Creating a higher level object

Stream: new members

[Abdullah Uyu]

I have the following axiomatization of a projective geometry. I proved some properties of projective geometries with this, but then, I want to say that these properties hold for the projectivization of a vector space already defined in the library. So, what I want is to lift up the level of abstraction.

structure ProjectiveGeometry (point : Type u) (ell: point → point → point → Prop)
where
l1 : ∀ a b, ell a b a
l2 : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3 : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

How to proceed from this? Is it possible to show that projectivization of a vector space is a model of this axiomatization? Or conversely, how can I create an axiomatization of which projectivization is a model? Can instances help me with this?

[Sabrina Jewson]

Not familiar with projective geometry, but I imagine you’d prove something like:

example [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : ProjectiveGeometry v.submodule (fun a b c ↦ Collinear K {a, b, c}) := sorry

(nevermind, I’m not sure that’s correct… it states that each element of the projectivization is a projective geometry, which I don’t think is what you want. I can’t get the correct version to work, because Submodule is not an AddGroup and so Collinear is refusing to typecheck)

instances are only useful if your ProjectiveGeometry is a class to begin with.

[Abdullah Uyu]

Ah I see. Yes, I want each Projectivization to be ProjectiveGeometry.

[Abdullah Uyu]

But, this way of thinking is possible in Lean, right? Maybe I should try to translate this structure to a class, then. @Sabrina Jewson

[Sabrina Jewson]

Well, whether you want it to be a class depends on how you use it (whether you want it use it as a [] parameter).

Determining the correct type signature to use a different problem, you’d want to ask someone more knowledgable in this areä of maths.

[Abdullah Uyu]

I understand, thank you.

[Abdullah Uyu]

@Joseph Myers Could you take a look at this?

[Abdullah Uyu]

You had suggested that the Desargue's Property should first be proved generally and then the affine versions should be derived from it. I am trying to somehow create a framework for it.

[Matt Diamond]

@Abdullah Uyu are you trying to do something like this?

import Mathlib.LinearAlgebra.Projectivization.Basic

variable [DivisionRing K] [AddCommGroup V] [Module K V]

class ProjectiveGeometry (point : Type u) where
ell : point → point → point → Prop
l1  : ∀ a b, ell a b a
l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

-- Every Projectivization is a ProjectiveGeometry
instance : ProjectiveGeometry (Projectivization K V) :=
⟨
  sorry, -- define `ell` for Projectivization K V
  sorry, -- prove l1
  sorry, -- prove l2
  sorry  -- prove l3
⟩

[Joseph Myers]

I don't know enough about abstract projective geometry to advise on exactly what the general type class structure and associated API should look like.

[Abdullah Uyu]

Hopefully the above will work out. I am going to fill the sorries throughout the next week.

[Abdullah Uyu]

Matt Diamond said:

Abdullah Uyu are you trying to do something like this?

import Mathlib.LinearAlgebra.Projectivization.Basic

variable [DivisionRing K] [AddCommGroup V] [Module K V]

class ProjectiveGeometry (point : Type u) where
ell : point → point → point → Prop
l1  : ∀ a b, ell a b a
l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

-- Every Projectivization is a ProjectiveGeometry
instance : ProjectiveGeometry (Projectivization K V) :=
⟨
  sorry, -- define `ell` for Projectivization K V
  sorry, -- prove l1
  sorry, -- prove l2
  sorry  -- prove l3
⟩

I have a few questions regarding this:

• Why class but not a structure?
• ell went inside but not point, why?

[Filippo A. E. Nuccio]

Concerning your first question, a class is somewhat a special kind of structure that is taken into account by type-class inference: you can have a look at Chapter 7 of #mil. At any rate the above code would have worked equally well replacing class by structure. Concerning the second point, what do you mean by "went inside"?

[Abdullah Uyu]

Filippo A. E. Nuccio said:

Concerning your first question, a class is somewhat a special kind of structure that is taken into account by type-class inference: you can have a look at Chapter 7 of #mil. At any rate the above code would have worked equally well replacing class by structure. Concerning the second point, what do you mean by "went inside"?

I initially wrote the following. The suggestion above moves ell inside, but point stays. I meant what is special about ell or point?

structure ProjectiveGeometry (point : Type u) (ell: point → point → point → Prop)
where
l1 : ∀ a b, ell a b a
l2 : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3 : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

[Filippo A. E. Nuccio]

We would say that point and ell "contain data": they are honest gadgets (one is a type, the other is a yes/no check on three variables, implemented as a function). On the other hand, l1-l2-l3 are just propositions, so we are requiring that they hold. The key difference lies in "propositional irrelevance", saying that types in Prop behave differently because every such type contains at most one term (aka: all proofs of a certain proposition coincide), and this is not true for other types.

[Sabrina Jewson]

In general, to determine whether you choose to put something inside a class (“bundling”) or put it in the parameters (“unbundled”) is a choice with tradeoffs either way.

1. If there is more than one possible implementation, then it must go in the parameters. For example, point must be a parameter because there is more than one projective geometry in existence. If, hypothetically, a single type that represents a projective geometry could have multiple different ell functions, then ell should definitely be a parameter.
2. Otherwise, if there is only one implementation, but you need to easily enforce that it is _the same as something else_, one should use an _out parameter_. An example of this is Lean’s HAdd typeclass. It has three parameters, α, β and γ, representing the left-hand input, right-hand input and output types respectively. α and β are both normal parameters, because they can be any two types, but γ is an out parameter, because given two types that you’re adding together, there should only be one possible output type. γ could have also been bundled in the HAdd class itself — the reason they _don’t_ do this is that it allows functions like the following:

example {α β γ} [HAdd α β γ] [Inhabited γ] := /- whatever -/;

That is, we are easily able to place further restrictions on γ by adding more typeclasses to it. This would be harder if γ was bundled.

3. If you don’t need the above use-case, which is often the case for functions like ell, you should bundle it, including it in the typeclass itself, as in the code sample given.

[Abdullah Uyu]

Sabrina Jewson said:

In general, to determine whether you choose to put something inside a class (“bundling”) or put it in the parameters (“unbundled”) is a choice with tradeoffs either way.

1. If there is more than one possible implementation, then it must go in the parameters. For example, point must be a parameter because there is more than one projective geometry in existence. If, hypothetically, a single type that represents a projective geometry could have multiple different ell functions, then ell should definitely be a parameter.
2. Otherwise, if there is only one implementation, but you need to easily enforce that it is _the same as something else_, one should use an _out parameter_. An example of this is Lean’s HAdd typeclass. It has three parameters, α, β and γ, representing the left-hand input, right-hand input and output types respectively. α and β are both normal parameters, because they can be any two types, but γ is an out parameter, because given two types that you’re adding together, there should only be one possible output type. γ could have also been bundled in the HAdd class itself — the reason they _don’t_ do this is that it allows functions like the following:

example {α β γ} [HAdd α β γ] [Inhabited γ] := /- whatever -/;

That is, we are easily able to place further restrictions on γ by adding more typeclasses to it. This would be harder if γ was bundled.

3. If you don’t need the above use-case, which is often the case for functions like ell, you should bundle it, including it in the typeclass itself, as in the code sample given.

Perfect, this makes complete sense. Thank you so much.