Structure defined for Desarguesian proj plane: has_coe_to...

Stream: general

[Eric Wieser]

Thinking about this a bit more, I'd recommend you replace

def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂}

with

-- this lets you write `{x : proj_plane_div_config P L} (x : c)`
instance : has_coe_to_sort (proj_plane_div_config P L) _ :=
{ coe_sort := \lam c, {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂} }

[Eric Wieser]

Then to define addition you should fill in

instance (c : proj_plane_div_config P L) : has_add c :=
{ add := sorry }

[Quinn Culver]

That's throwing

type expected at
  has_coe_to_sort (proj_plane_div_config P L)
term has type
  out_param (Sort ?) → Sort (max (max 1 (u+1)) ?)

[Eric Wieser]

Well, that tells you there's an argument missing; so try adding a _

[Eric Wieser]

If you get the error message that ends with term has type Y → Z at foo x, usually that means you should have written foo x y. That's a super important error message to know how to read.

[Reid Barton]

Eric Wieser said:

Thinking about this a bit more, I'd recommend you replace

def the_div_ring (c : proj_plane_div_config P L) : Type* := {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂}

with

-- this lets you write `{x : proj_plane_div_config P L} (x : c)`
instance : has_coe_to_sort (proj_plane_div_config P L) :=
{ coe_sort :=  {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂} }

This feels deeply strange to me.

[Eric Wieser]

@Reid Barton: The config is meaningless besides defining the division ring, isn't it? Why is this different to how we handle subgroup in mathlib (which presumably you do not regard as strange)?

[Reid Barton]

This is more like you define a has_coe_to_sort on n : nat that returns zmod n.

[Reid Barton]

A subgroup is a subgroup and a subgroup has elements that are the members of the subgroup--that seems obvious.

[Eric Wieser]

Does proj_plane_div_config P L have any use besides creating this division ring?

[Reid Barton]

I mean it is just some data of fixing some points that aren't badly chosen

[Eric Wieser]

Because certainly nat has uses besides creating zmod n

[Eric Wieser]

Reid Barton said:

I mean it is just some data of fixing some points that aren't badly chosen

A subgroup is just some data fixing a set of values that are well chosen

[Reid Barton]

No, this is absurd but I don't know how to explain why.

[Reid Barton]

Maybe you can figure it out.

[Eric Wieser]

Would defining

def proj_plane_div_config.carrier : set P :=
{x : P | x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂}

instance : has_coe_to_sort (proj_plane_div_config P L) :=
{ coe_sort :=  \lam c, c.carrier }

feel less absurd to you? That's the connection to subgroup I'm trying to make

[Reid Barton]

It cannot be called "carrier"

[Eric Wieser]

Is it the fact that we're putting a + on c.carrier that is independent of the + that might exist on the underlying P that makes you uneasy?

[Reid Barton]

Again it is just like defining nat.carrier

[Reid Barton]

That's not what the word means

[Eric Wieser]

Let me try and justify it from another direction. I claim this is reasonable:

def proj_plane_div [configuration.is_desarguesian P L]
  (a₁ a₂ c₁₃ c₂₃ : P) (ha₁a₂ : a₁ ≠ a₂) (hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃) : Type* :=
{x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂} }

def foo : proj_plane_div a₁ a₂ c₁₃ c₂₃ ha₁a₂ hnoncol := sorry

so using coe_sort is just a syntactic grouping for convenience, to avoid passing around 6 arguments

structure proj_plane_div [configuration.is_desarguesian P L] :=
(a₁ a₂ c₁₃ c₂₃ : P)
(ha₁a₂ : a₁ ≠ a₂)
(hnoncol : four_points_no_three_collinear L a₁ a₂ c₁₃ c₂₃)

instance : has_coe_to_sort (proj_plane_div P L) _ :=
{ coe_sort := λ c, {x : P //  x ∈ (mk_line c.ha₁a₂ : L) ∧ x ≠ c.a₂} }


def foo {c : proj_plane_div P L} : c := sorry

[Reid Barton]

What's a proj plane div?

[Reid Barton]

The name has no connection to the definition. And two of the points are not even used.

[Eric Wieser]

I'm afraid I have no idea what the "real" names for the things that @Quinn Culver is talking about here are

[Quinn Culver]

I assume by "real" you mean "conventional" @Eric Wieser ?

[Quinn Culver]

The sources I've seen do not give it a name. But I don't have much experience in the field.

[Quinn Culver]

Need/should I clarify the definition of the division ring that's associated to any desarguesian projective plane?

[Reid Barton]

The math is something like this. We have our favorite projective plane and we fix some points on it. We are going to give a division ring on the line through two of the points (with one of them removed). We need the other two points to define (most of) the ring operations.

[Eric Wieser]

https://ncatlab.org/nlab/show/projective+plane#equivalence_of_synthetic_and_analytic suggests the structure be called "scalar"

[Reid Barton]

The choice of some points is not a ring, it's a choice of some points.

[Reid Barton]

I think the thing you linked to is not exactly the approach that Quinn is taking

[Eric Wieser]

Indeed, I can't find a reference that matches Quinn's approach because I don't know what to search for!

[Quinn Culver]

ftpg.pdf

[Notification Bot]

35 messages were moved from this topic to #general > Structure defined for Desarguesian proj plane: has_coe_to... by Eric Wieser.

[Notification Bot]

3 messages were moved here from #general > Structure defined for Desarguesian proj plane: has_coe_to... by Eric Wieser.

[Notification Bot]

3 messages were moved from this topic to #general > Structure defined for Desarguesian proj plane by Eric Wieser.