# Zulip Chat Archive

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