Reasoning about quotients

Stream: maths

[Ching-Tsun Chou]

I am reading chapter 7 of "Mathematics in Lean" and am somewhat mystified by the proofs on lines 110-127 of:

https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean

In particular, I have the following questions:

(1) At the beginning of the proof for "mul", the proof state is like this:

image.png

First of all, I do not know how to read the goal after the ⊢. Second, I don't understand how the "rintro" on line 112 matches the goal.

(2) After the "rintro", the goal looks like this:

image.png

I understand what the goal means (namely, a1a2 and b1b2 should satisfy the relation Setoid.r). But I don't understand how the "refine" tactic works here.

(3) The arguments of the "rintro" tactic son lines 118, 125, and 127 are enclosed in angle brackets. I understand what is happening: we are introducing variables for representatives of the equivalence classes, not the equivalence classes themselves. But I don't understand why the angle brackets have such capabilities.

[Violeta Hernández]

Quotient.map₂'

[Violeta Hernández]

Honestly I'm confused too, I hadn't come across ⇒ before...

[Violeta Hernández]

The angle brackets don't have the capability of introducing representatives for equivalence classes. I think that's being done implicitly by Quotient.map₂'.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

What I presume Quotient.map₂' does is: given a function f : α → β → γ, and a guarantee that equivalent terms in α and β yield equivalent terms in γ, it lifts the function to the respective quotients

[Violeta Hernández]

What the angle brackets are actually destructing are the proofs that a₁, b₁ and a₂, b₂, are equivalent

[Shanghe Chen]

I am reading this currently too and I found this first part and second part is hard to understand too. But for reading Setoid.r ⇒ Setoid.r ⇒ Setoid.r I find that the fact ⇒ is right associated quite helpful. Hence it’s same as Setoid.r ⇒ (Setoid.r ⇒ Setoid.r) and then unravel the definition for ⇒ twice and it gives the same intuition in math

[Shanghe Chen]

But for the solution for mul_assoc and one_mul etc, I am surprised that why rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ works too. Is there some special logic in the implementation of rintro for quotient?

[Eric Wieser]

Shanghe Chen said:

Is there some special logic in the implementation of rintro for quotient?

Yes, there is

[Shanghe Chen]

after the rintros the solution uses apply Quotient.sound. It’s amazing the Quotient sound is applicable. It seems even applied multiple time without using repeat

[Shanghe Chen]

Eric Wieser said:

Shanghe Chen said:

Is there some special logic in the implementation of rintro for quotient?

Yes, there is

which result does it relies on?

[Shanghe Chen]

before checking the solution in MIL I also tried to use Quotient.inductionOn₃' but it seems giving a dead end for me:

import Mathlib
import Mathlib.GroupTheory.QuotientGroup.Basic

set_option autoImplicit true


def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where
  r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x*w = y*z
  iseqv := {
    refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
    symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
    trans := by
      sorry
  }

instance [CommMonoid M] : HasQuotient M (Submonoid M) where
  quotient' := fun N ↦ Quotient N.Setoid

def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N := Quotient.mk N.Setoid

instance [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
  mul := Quotient.map₂' (· * ·) (by
      sorry
        )
  mul_assoc := fun a b c => Quotient.inductionOn₃' a b c (by
     -- seems dead end here
     intro a b c
     -- failed to synthesize HMul
     -- #check (Quotient.mk'' a * Quotient.mk'')
     sorry)
  one := QuotientMonoid.mk N 1
  one_mul := by
      sorry
  mul_one := by
      sorry

I cannot even use the symbol * in the proof for mul_assoc after it

[Ching-Tsun Chou]

Regarding my question (2), I noticed that the Setoid.r in the goal can be simplified away and then the "refine" can be replaced by two sets of "use" followed by "simp"; see lines 92-94 here:

https://github.com/ctchou/mathematics_in_lean/blob/main/MIL/C07_Hierarchies/S03_Subobjects_ctchou.lean

[Patrick Massot]

I am pretty sure the goal didn’t look like that when I wrote this chapter. Something must have changed in between :sad:

[Ching-Tsun Chou]

Should I create an issue at the source repo https://github.com/avigad/mathematics_in_lean_source ?

[Patrick Massot]

Yes please

[Ching-Tsun Chou]

https://github.com/avigad/mathematics_in_lean_source/issues/261

[Benjamin Jones]

Shanghe Chen said:

before checking the solution in MIL I also tried to use Quotient.inductionOn₃' but it seems giving a dead end for me:

...
I cannot even use the symbol `*` in the proof for `mul_assoc` after it

re: the comment above about rintro magic, regular intro along with the surjectivity of the quotient map gets you to effectively the same goal:

  mul_assoc := by
      intro a b c
      let ⟨a', ha'⟩  := quotient_map_surjective N a
      let ⟨b', hb'⟩  := quotient_map_surjective N b
      let ⟨c', hc'⟩  := quotient_map_surjective N c
      repeat rw [← ha', ← hb', ← hc']
      -- goal is now:
      -- ⊢ QuotientMonoid.mk N a' * QuotientMonoid.mk N b' * QuotientMonoid.mk N c' = QuotientMonoid.mk N a' * (QuotientMonoid.mk N b' * QuotientMonoid.mk N c')

Resolving * as a binary op on M / N in the goal can be done by naming the instance, say monoidInstMN and then using that as the namespace, i.e. (monoidInstMN N).mul. There might be a simpler way. I didn't end up needing to refer to * explicitly on M / N.

instance monoidInstMN [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
...
  mul_assoc := by
    ...
          have : ∀ (a' b' x': M), a' * b' = x' ↔ (monoidInstMN N).mul (QuotientMonoid.mk N a') (QuotientMonoid.mk N b') = QuotientMonoid.mk N x' := by
            sorry

The key thing I got hung up on in this exercise was the use of Quotient.sound. I think if that was explained in the paragraph above the exercise it would be more straightforward.

[Chris Wong]

Regarding (1). Since the funny construction appears to be fully applied, I suspect that dsimp would expand it out.