## Stream: general

### Topic: quotient.induction_on order of variables

#### 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?

#### Kevin Buzzard (Feb 06 2019 at 16:01):

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

#### 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?

#### Patrick Massot (Feb 06 2019 at 16:23):

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

#### 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

#### 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.

#### 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.

#### 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"

#### 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₂'.

#### 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.

#### Chris Hughes (Feb 06 2019 at 17:08):

quotient.induction_on' and quotient.induction_on₂'

#### Kevin Buzzard (Feb 06 2019 at 17:13):

The variables are in the wrong order for me with _on

#### 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