Empty torsors

Stream: maths

[Yaël Dillies]

@Joseph Myers, would it make sense to allow P to be empty in add_torsor G P. This is currently impossible due to docs#add_torsor.nonempty. In fact, this instance is dangerous as it loops with docs#affine_subspace.add_torsor and, as noted by @Paul Reichert, this means not all affine subspaces are add torsors.

[Sebastien Gouezel]

It wouldn't make sense from a mathematical point of view, at least for the usual notion: an add_torsor G P is supposed to be a copy of G in which you have forgotten the identity.

[Joseph Myers]

My guess is that the main effect would be to move around where nonempty hypotheses are needed. I ran into that dangerous instance recently in #16339, but my best guess as to the right way to avoid the typeclass loop would have been "make [nonempty P] an argument to add_torsor" rather than "remove the nonempty requirement".

[Paul Reichert]

It might be useful to have a class add_pseudo_torsor, lacking the nonzero requirement. There are a lot of properties holding for pseudo-torsors and they have the nice property that there is a well-defined closure operator -- even the empty set has a well-defined closure.
However, it seems hard to tell Lean something like "an add_torsor is an add_pseudo_torsor with a nonzero instance" without producing a loop because we can produce add_torsor instances from add_pseudo_torsorinstances and vice versa. Are there some "tricks" to avoid this problem, and is this even a sensible approach?

class add_pseudo_torsor (G : out_param Type*) (P : Type*) [out_param $ add_group G]
  extends add_action G P, has_vsub G P :=
(vsub_vadd' : ∀ (p1 p2 : P), (p1 -ᵥ p2 : G) +ᵥ p2 = p1)
(vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g)

class add_torsor (G : out_param Type*) (P : Type*) [out_param $ add_group G]
  extends add_pseudo_torsor G P :=
[nonempty : nonempty P]

instance nonempty_pseudo_torsor {G P : Type*} [add_group G] [add_pseudo_torsor G P] [nonempty P] :
add_torsor G P := ⟨⟩

attribute [instance, priority 100, nolint dangerous_instance] add_torsor.nonempty

-- maximum class-instance resolution depth reached
instance add_group_is_add_torsor (G : Type*) [add_group G] :
  add_torsor G G :=
{ vsub := has_sub.sub,
  vsub_vadd' := sub_add_cancel,
  vadd_vsub' := add_sub_cancel }

[Paul Reichert]

For example, I'd like to tell Lean "don't worry; you already know the add_pseudo_torsor instance obtained from the add_torsor instance obtained from the add_pseudo_torsor instance and so you can ignore it"

[Kevin Buzzard]

Following preprime and preconnected it should perhaps be called pretorsor.

[Joseph Myers]

If we have a class of pretorsors I'd be inclined not to have a separate one for torsors; just add nonempty hypotheses to the few lemmas or definitions that genuinely need a torsor not a pretorsor and where nonempty can't be deduced from the other hypotheses.

[Paul A. Reichert]

Okay, this post is already outdated, but for reference:

This branch is a proof of concept of the approach. I made the above-mentioned instance a def to avoid the problems. The build succeeded but this approach would introduce a new kind of boilerplate:

variables {G : Type*} {P : Type*} {G' : Type*} {P' : Type*} [add_group G] [add_group G']

instance [add_pseudo_torsor G P] [add_pseudo_torsor G' P'] : add_pseudo_torsor (G × G') (P × P') :=
{ vadd := λ v p, (v.1 +ᵥ p.1, v.2 +ᵥ p.2),
  zero_vadd := λ p, by simp,
  add_vadd := by simp [add_vadd],
  vsub := λ p₁ p₂, (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2),
  vsub_vadd' := λ p₁ p₂, show (p₁.1 -ᵥ p₂.1 +ᵥ p₂.1, _) = p₁, by simp,
  vadd_vsub' := λ v p, show (v.1 +ᵥ p.1 -ᵥ p.1, v.2 +ᵥ p.2 -ᵥ p.2)  =v, by simp }

instance [add_torsor G P] [add_torsor G' P'] : add_torsor (G × G') (P × P') :=
{ nonempty := prod.nonempty }

If this is the way to go, I'd have to look for required add_torsor instances throughout mathlib and relax them to add_pretorsor instances.

[Paul A. Reichert]

Joseph Myers said:

If we have a class of pretorsors I'd be inclined not to have a separate one for torsors; just add nonempty hypotheses to the few lemmas or definitions that genuinely need a torsor not a pretorsor and where nonempty can't be deduced from the other hypotheses.

Yes, this seems also reasonable; at the same time, I understand concerns that torsors are just a bit more familiar for mathematicians than pretorsors. Let me just emphasize that this is just a proposal, we can also reject the whole pretorsor thing if it turns out to complicate things.

[Yaël Dillies]

From a purely hierarchy design point of view, it would be cleaner to not make nonempty P a field of add_torsor.

[Kevin Buzzard]

Just to be clear, if you're saying "in Lean torsors should be allowed to be empty" then torsors are nonempty by definition and you can't change that (like you can't decide that 1 is going to be prime in Lean). But if you're saying something else then sorry I misunderstood :-)

[Yaël Dillies]

I'm saying that maybe the way to say "P is a torsor" should be [add_torsor G P] [nonempty P] rather than [add_torsor G P].

[Yaël Dillies]

Even though that's not what I'm arguing about, univ isn't a filter but we still made it one in Lean :wink:

[Johan Commelin]

In the real world, univ isn't a filter for the exact same reason that ⊤ isn't an ideal. Yet we made ⊤ an ideal in Lean anyway. /s

[Kevin Buzzard]

The difference here is that it is known that mathematicians in the literature have two opinions on what a filter is, like they have two opinions on what the natural numbers are. As far as I know they only have one opinion on what a torsor is, like they only have one opinion on what a prime number is