Where to start to learn Mathlib?

Stream: new members

[l1mey]

I've been programming and proving in Lean for a while and have a decent amount of experience with the tactics, typeclasses, conventions in the standard library, metaprogramming.

However, I'm having a hard time understanding the algebraic hierarchy as well as the encoding of a couple theorems. For example from following mathematics in Lean, I'm trying to prove the first isomorphism theorem from a paper proof:

import Mathlib

noncomputable section

/- our two groups G and H -/
variable {G H : Type*} [Group G] [Group H]

def FIT (φ : G →* H) : G ⧸ φ.ker ≃* φ.range := {
  toFun := ???
}

Looking at QuotientGroup.quotientKerEquivRange which is the theorem I'm trying to prove that already exists, which I'm guessing isn't encoded as an "is isomorphic" relation, but instead just provides the isomorphism.

This would be okay but I'm trying to navigate how this is all defined in the algebraic hierachy. When I press Ctrl-space inside the structure there are a couple fields. The toFun part is a function from G ⧸ φ.ker → φ.range where G ⧸ φ.ker : Type and φ.range : Type. But I don't know how to actually construct the canonical isomorphism (the one that takes gK ↦ φ(g)), since these are opaque types which I can't extract the representative of the coset in the domain. I'm assuming most of this is hidden behind typeclasses.

Above is sort of my thought process, but my question is that since Mathlib is such a large library (it's software afterall) and that a lot of technical choices are made when encoding definitions in such a way that they're nice to use, where could you begin to comprehend it all?

I am an undergraduate at mathematics but self study ahead, if that matters. I was also thinking about trying to reverse engineer some of the definitions, and recreate my own subset of Mathlib (thinking from a software engineer perspective). How about it?

[Weiyi Wang]

I am not good at providing general guides, so just commenting on small pieces...

since these are opaque types which I can't extract the representative of the coset in the domain

Groups and quotient groups are not so opaque and you can unfold a lot of things to see how it works under the hood. It is not a recommended code style for serious contribution, but for helping your own understanding it is fine to do. For example, the quotient group, if you unfold the definition a few times, is eventually the docs#Quotient type, from which you can get a representative by calling docs#Quotient.out, which can lead to valid proof and construction. Though, constructions using Quotient.out is very cumbersome, so what one usually does is to use various recursion/induction helper to effectively get a representative elegantly. For example, docs#QuotientGroup.quotientKerEquivRange uses (again after unfolding definitions a few times) docs#QuotientGroup.lift, which is ultimately is docs#Quotient.liftOn. By reading its signature, it basically says you give it a function that accepts representatives, and it will return you a lifted function that accepts quotient elements.

[Niels Voss]

To answer some of your other questions:

• #mil has some pretty good guides and exercises on particular topics in Mathlib. It is much less foundational than #tpil and is more applied.
• You can use loogle or a semantic search engine (e.g. leansearch, lean explore, lean dex) to search through theorems quickly. This will indirectly teach you the algebraic hierarchy as you can see what typeclasses are needed for certain theorems.
• There's this library note: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/HierarchyDesign.html#The-algebraic-hierarchy, but it is more of a guide on how to extend the hierarchy than how to navigate it.

I think most mathlib contributors learned the hierarchy as a result of working with mathlib, rather than because there was explicit documentation on the algebraic hierarchy.

[Kevin Buzzard]

A quotient group isn't cosets, it's an opaque type satisfying the universal property of quotients. To define a function from a quotient you use a function called lift, feeding it a function from the big type and supplying the universal property (that it's constant on equivalence classes).

[Riccardo Brasca]

Let's do it step by step and let's concentrate on the toFun field, that is the bare function (then it remains to prove that it respects multiplication and to provide the inverse, or to prove injectivity and surjectivity), so let's define

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := sorry

I am going to write several times the same line, adding missing pieces at each time. Usually it's not a good idea to write definition in tactic mode, but at the beginning you can do it to have a working infoview, and go back to term mode at the end. So here we are

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := by
  sorry

Of course we want to take (x : G ⧸ φ.ker).

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := by
  intro x
  sorry

Now you see that the goal is ⊢ ↥φ.range: we need to specify the image of x. The point is that φ.range is of type φ.range : Subgroup H: it is a subgroup of H, so it's term are pairs given by a term of H and a proof that this term belongs to φ.range. We can see this as follows

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := by
  intro x
  refine ⟨?_, ?_⟩
  · sorry
  · sorry

In the first sorry the goal is H: we need to specify the image of x. Mathematically the point is that we descend φ to the quotient, since obviously it respects the equivalence relation. In Lean we always say "lift" instead of "descend", and for example one can use docs#Quotient.liftOn' (it gives a better version of h than docs#Quotient.liftOn).

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := by
  intro x
  refine ⟨?_, ?_⟩
  · refine Quotient.liftOn x φ ?_
    sorry
  · sorry

Now the sorry is the fact that φ respects the equivalence relation, and this is not very difficult.

def FIT (φ : G →* H) : G ⧸ φ.ker → φ.range := by
  intro x
  refine ⟨?_, ?_⟩
  · refine Quotient.liftOn' x φ ?_
    intro a b h
    rw [QuotientGroup.leftRel_apply] at h
    have h₁ := φ.ker.inv_mem h
    simp only [mul_inv_rev, inv_inv] at h₁
    have := Subgroup.Normal.mem_comm inferInstance h₁
    rwa [← MonoidHom.div_mem_ker_iff, div_eq_mul_inv]
  · sorry

Can you see how to finish? Of course I am doing things very much by hand, and mathlib approach is much more granular, so you don't see any of this, but the idea is more or less the same.

[l1mey]

I appreciate the responses, over today I finished a proof based on some of the ideas that have been said. I know Mathlib does it differently (especially using by to construct data, which I've never done before but it made it easy to follow), but I've tried to follow my paper proof as much as possible. Below is an #mwe:

import Mathlib

set_option linter.style.emptyLine false

noncomputable section

/- our two groups G and H -/
variable {G H : Type*} [Group G] [Group H]

/- we know φ is a homomorphism -/
variable {φ : G →* H}

lemma eq_iff_mem_ker (g₁ g₂ : G)
    : φ g₁ = φ g₂ ↔ g₁⁻¹ * g₂ ∈ φ.ker := by

  /- φ g₁ = φ g₂ -/
  rw [← inv_mul_eq_one, ← map_inv, ← map_mul]
  rw [MonoidHom.mem_ker]

/-- Canonical Homomorphism π : G ⧸ ker φ → φ(G). -/
def π : G ⧸ φ.ker → φ.range := by
  intro x

  refine ⟨?_, ?_⟩
  · refine Quotient.lift φ ?_ x
    intro g₁ g₂ h
    /- g₁ ≈ g₂ → φ g₁ = φ g₂ -/

    /- we have g₁K = g₂K if and only if g₁⁻¹ g₂ ∈ K -/
    have hrel : g₁⁻¹ * g₂ ∈ φ.ker := by
      rwa [← QuotientGroup.leftRel_apply]

    rwa [eq_iff_mem_ker]

  · induction x using Quotient.inductionOn with
    | h a =>
      rw [Quotient.lift_mk]
      rw [MonoidHom.mem_range]
      use a

def π_hom : G ⧸ φ.ker →* φ.range := {
  toFun := π
  map_one' := by
    rw [π, Subgroup.mk_eq_one, ← QuotientGroup.mk_one, Quotient.lift_mk]

    /- φ 1 = 1     (φ is a homomorphism) -/
    exact MonoidHom.map_one φ

  map_mul' := by
    intro x y

    /- π (g₁ * g₂) = π g₁ * π g₂ -/
    simp only [π, MulMemClass.mk_mul_mk, Subtype.mk.injEq]

    induction x using Quotient.inductionOn with
    | h g₁ =>
    induction y using Quotient.inductionOn with
    | h g₂ =>

    rw [← QuotientGroup.mk_mul]
    repeat rw [Quotient.lift_mk]

    /- φ (g₁ * g₂) = φ g₁ * φ g₂     (φ is a homomorphism) -/
    exact MonoidHom.map_mul φ g₁ g₂
}

theorem π_bijective : Function.Bijective (π : G ⧸ φ.ker → φ.range) := by
  constructor
  · intro x y h

    /- π (g₁ * g₂) = π g₁ * π g₂ -/
    induction x using Quotient.inductionOn with
    | h g₁ =>
    induction y using Quotient.inductionOn with
    | h g₂ =>

    simp only [π, Quotient.lift_mk, Subtype.mk.injEq] at h

    rw [QuotientGroup.eq]
    rwa [eq_iff_mem_ker] at h

  · intro y
    /- we know that y ∈ φ.range, hence ∃g, φ g = y -/
    obtain ⟨g, hg⟩ := y.property

    unfold π
    rw [QuotientGroup.exists_mk]; use g

    ext
    simpa

def FIT : G ⧸ φ.ker ≃* (φ.range) := by
  exact MulEquiv.ofBijective π_hom π_bijective

/--
info: 'FIT' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms FIT

I know the proof is quite ugly, but I hope it's workable enough to be read. I have a couple questions:

1. What is the difference between Quotient.mk and QuotientGroup.mk ? Sometimes I see either ⟦g₁⟧ : Quotient (QuotientGroup.leftRel φ.ker) or ↑g : G ⧸ φ.ker (mentioned in the same order) used in the argument of a Quotient.lift where a G ⧸ φ.ker would be expected.

2. When constructing the homomorphism G ⧸ φ.ker →* φ.range, you provide the function and a proof that the function preserves the one and multiplication. Is there a reason for the proof of map_one ? I thought you could prove map_one straight from the map_mul (the defn. of a homomorphism) hypothesis?

3. What is the best way to avoid induction x using Quotient.inductionOn to extract out a representative g : G from an element x : G ⧸ φ.ker ?

A lot of my time was spent searching around for definitions and theorems, and guessing their names. Could anyone also be able to provide some advice as well? I appreciate it.

[l1mey]

In (1) it might be a definitional equality? I think I remember seeing a couple notes in the documentation about some things being definitional equalities. If someone could let me know in the QuotientGroup API what parts are designed around a definitional equality that would be good.