Zulip Chat Archive

Stream: maths

Topic: quotients and lifts for functions of arbitrary arity


view this post on Zulip William DeMeo (Dec 02 2018 at 04:31):

I'm trying to learn how to implement general quotient structures. Unfortunately, I've only been able to figure out how to lift unary operations. How does one lift operations of arbitrary arity?

More specifically, here's what I'm trying to do.

Given a type α\alpha, and an "arity" type ρ\rho, an operation on α\alpha of arity ρ\rho has the following type signature:
f:(ρα)αf : (\rho \to \alpha) \to \alpha.

Now suppose I have an equivalence relation r:ααPropr : \alpha \to \alpha \to \mathsf{Prop}, and I want to lift ff to a ρ\rho-ary operation f~:(ρα/r)α/r\tilde{f} : (\rho \to \alpha/r) \to \alpha/r. That is, f~\tilde{f} should be a ρ\rho-ary operation on the quotient α/r\alpha / r. It's obvious how to express this mathematically:

f~(a/[[r]])=(fa)/r\tilde{f} (a/[[r]]) = (f a)/r,

where [[r]][[ r ]] is the binary relation on ρα\rho \to \alpha induced by rr. That is, a[[r]]ba \mathrel{[[ r ]]} b iff i,(ai)r(bi)\forall i, (a i) \mathrel{r} (b i).

For example, if ff is nn-ary, then f~\tilde{f} maps an nn-tuple (a0/r,,an1/r)(a_0/r, \ldots, a_{n-1}/r) of rr-classes to the rr-class f(a0,,an1)/rf(a_0, \ldots, a_{n-1})/r.

I got this to work when ff is unary (so, f:ααf : \alpha \to \alpha), by first defining the projection πf:αα/r\pi f : \alpha \to \alpha/r as quot.mk r (f a), and then using the built in quot.lift, defined in quot.lean of the standard library. (The code for that is below, but it's not pretty.)

Unfortunately, this doesn't work for higher arity operations because quot.lift expects a relation r:ααPropr : \alpha \to \alpha \to \mathsf{Prop} and a proof of ab,arb(fa)/r=(fb)/r\forall a b, a \mathrel{ r } b \to (f a)/r = (f b)/r. But in the higher arity case, to say that the operation f:(ρα)αf : (\rho \to \alpha) \to \alpha "respects" rr means the following:

(ab:ρα),(i,r(ai)(bi))(fa)/r=(fb)/r\forall (a b : \rho \to \alpha), (\forall i, r (a i) (b i)) \to (f a)/r = (f b)/r

If you provide quot.lift with that as the proof of "respecting r", the resulting lift will not be what we want.

Any ideas, pointers, suggestions would be much appreciated. Thanks!

Here's the code for the unary case. There's probably an easier way to do this, and suggestions are welcome... but I'm more interested in the general case.

  parameters {α : Type*} {ρ : Type*}
  local notation a`/`r := quot.mk r a

  def π (f : α  α) (r : α  α  Prop) : α  quot r := λ a, (f a) / r

  def compatible_unary (f : α  α) (r : α  α  Prop) :=  a b, r a b  r (f a) (f b)

  lemma resp_proj_of_compatible_unary
  (f : α  α) (r : α  α  Prop) (h : compatible_unary f r) :
   a b, r a b  (f a)/r = (f b)/r :=
  assume a b (h₀ : r a b),
  have h₃ : r (f a) (f b), from h a b h₀,
  show (f a)/r = (f b)/r, from quot.sound h₃

  def lift_proj (f : α  α) (r : α  α  Prop) (h : compatible_unary f r) :
  quot r  quot r :=
  quot.lift (π  f r) (resp_proj_of_compatible_unary f r h)

view this post on Zulip Chris Hughes (Dec 02 2018 at 06:17):

One way of doing this is to put a relation on ρα\rho \rightarrow \alpha defined as λxy,a:α,r(x(a))(y(a))\lambda x y, \forall a : \alpha, r (x (a)) (y( a)). I don't think you can define a function of this type quotient.lift_onₙ (x : Π a : α, quotient (s a)) (f : (Π a : α, β a) → γ) (h : ∀ x₁ x₂ : Π a, β a, (∀ a, x₁ a ≈ x₂ a) → f x₁ = f x₂) : γ without choice though. There is something in data.fintype that let's you do it computably when your indexing type is finite, but the fact that that's only defined on fintypes suggestsit might not be possible on infinite types.

view this post on Zulip Reid Barton (Dec 02 2018 at 15:08):

@William DeMeo You can use quotient.choice in mathlib to turn a product of quotients into a quotient of the product, and then lift on that to define a function.

view this post on Zulip Reid Barton (Dec 02 2018 at 15:09):

As far as I know you can't do this computably/without axioms, though it would be possible to implement by extending Lean.

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 15:11):

By "without axioms" you just mean "without some standard axioms which are inbuilt into Lean but which break computability", right?

view this post on Zulip Reid Barton (Dec 02 2018 at 15:12):

Yes

view this post on Zulip William DeMeo (Dec 02 2018 at 16:07):

@Chris Hughes Great, thanks for the hints! I will look at data.fintype. I'd like to be able to do this computably at least for finitary operations. (By the way, just to be sure I understand your suggestions, I think you meant to put ρ\rho in place of α\alpha in the two places where α\alpha appears... correct?) Thanks again for your help!

view this post on Zulip Chris Hughes (Dec 02 2018 at 16:08):

Yes I did mean to put rho instead of alpha

view this post on Zulip William DeMeo (Dec 02 2018 at 16:11):

@William DeMeo You can use quotient.choice in mathlib to turn a product of quotients into a quotient of the product, and then lift on that to define a function.

Thanks @Reid Barton , maybe I'll try that if after I get it to work computably for fintype.

view this post on Zulip Reid Barton (Dec 02 2018 at 16:12):

https://github.com/leanprover/mathlib/commit/ddbb81389b6d6cd3d0395f474896dcd59e1ed9e4

view this post on Zulip Reid Barton (Dec 02 2018 at 16:12):

added both quotient.choice and a computable finset version

view this post on Zulip William DeMeo (Dec 02 2018 at 17:07):

added both quotient.choice and a computable finset version

Awesome! Thanks @Reid Barton I'll see if I can use those types to do exactly what I want. If not, I'll have to roll my own, but it's good to see these examples that show how things should be done.


Last updated: May 11 2021 at 16:22 UTC