Zulip Chat Archive

Stream: general

Topic: quotient.induction_on order of variables


view this post on Zulip Kevin Buzzard (Feb 06 2019 at 15:53):

I noticed something when descending proofs from a function on an object to a function on a quotient object. In short: I have v : R -> X satisfying some axioms, and it is constant on cosets of J so it descends to a function vbar: R/J -> X. I now need to prove that vbar satisfies the axioms which v satisfies, and in each case the proof is "this follows immediately". But look at my proofs:

  map_zero := map_zero v,
  map_one := map_one v,
  map_mul := λ x y, quotient.induction_on₂' x y $
    λ a b, -- my goal does not even mention x and y
    map_mul _ _ _,

The function map_mul wants two elements x and y of R/J and then a proof that vbar(x*y)=vbar(x)*vbar(y). I eat x and y and then apply one of these standard quotient.induction_on₂' functions which instantly wants x and y as input, plus a proof that for all a,b in R, v(a*b)=v(a)*v(b). My goal does not even mention x and y, they have already been used.

So I defined a new quotient.induction_on₂'' which asks for the proof first (it is simply re-ordering the inputs):

definition quotient.induction_on₂'' :
 {α : Sort*} {β : Sort*} {s₁ : setoid α} {s₂ : setoid β}
{p : quotient s₁  quotient s₂  Prop}
-- this first
(h :  (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂))
-- then these
(q₁ : quotient s₁) (q₂ : quotient s₂), p q₁ q₂
:= λ α β s₁ s₂ p h q₁ q₂, quotient.induction_on₂' q₁ q₂ h

and now for map_add I could just write

map_add := quotient.induction_on₂'' (λ a b, map_add _ _ _)

People here are smart and they must have realised this before. Is my quotient.induction_on₂'' function already in Lean or mathlib?

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:01):

Hmm, does _on mean "I am going to ask for the variables first", like rec_on?

view this post on Zulip Rob Lewis (Feb 06 2019 at 16:03):

Hmm, does _on mean "I am going to ask for the variables first", like rec_on?

Yes, usually. Without looking at the details, is quotient.ind₂ what you want?

view this post on Zulip Patrick Massot (Feb 06 2019 at 16:23):

@Kevin Buzzard Did you trying using more rintro magic as I told you?

view this post on Zulip Patrick Massot (Feb 06 2019 at 16:24):

as in

import ring_theory.ideals

variables (R : Type) [comm_ring R] (I : ideal R)

example :  x : I.quotient, true :=
begin
  rintro x,
  trivial
end

look at tactic state after the first line

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:29):

I am not even in tactic mode; I want to say "this is trivial" as quickly as possible.

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:31):

I wasn't in front of Lean when the penny dropped about _on but now I am, and I think that the ' also has a meaning -- ' means "use quotient.mk' not quotient.mk". I am only just getting to the bottom of things. Maybe I want quotient.ind₂'? Is that the name of this function? It doesn't appear to be there.

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:33):

So apparently quotient.mk means "infer the equivalence relation using type class inference" and quotient.mk' means "infer it using unification"

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:35):

In my situation I have a quotient of a ring by an ideal, and rings have lots of ideals, so I guess I will not be using type class inference. This seems to put me in the ' world. So currently my belief is that the function I want should be called quotient.ind₂'.

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 16:40):

And I can't find this. Have I got this straight? My conclusion is that I should write a short PR adding quotient.ind' and quotient.ind₂' and maybe a 3 variable version, to data/quot.lean.

view this post on Zulip Chris Hughes (Feb 06 2019 at 17:08):

quotient.induction_on' and quotient.induction_on₂'

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 17:13):

The variables are in the wrong order for me with _on

view this post on Zulip Kevin Buzzard (Feb 06 2019 at 17:15):

#check @quotient.ind'
/-
quotient.ind' :
  ∀ {α : Sort u_5} {s₁ : setoid α} {p : quotient s₁ → Prop},
    (∀ (a : α), p (quotient.mk' a)) → ∀ (q : quotient s₁), p q
    -/
#check @quotient.induction_on'
/-
quotient.induction_on' :
  ∀ {α : Sort u_5} {s₁ : setoid α} {p : quotient s₁ → Prop} (q : quotient s₁),
    (∀ (a : α), p (quotient.mk' a)) → p q
    -/

I want the hypothesis before the quotient variables. I hope I've understood the rules for naming these functions correctly.


Last updated: May 09 2021 at 19:11 UTC