First Isomorphism Theorem

Stream: mathlib4

[brokkilisoup]

Hello, I'm a master student (new in Lean) trying to Re-proving First Isomorphism Theorem. I managed to give a proof of the First Isomorphism Theorem using the "lift" function and the code is the following

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.Perm.Subgroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.Subgroup.Basic

open QuotientGroup

theorem first_isomorphism_theorem {G : Type*} [Group G] {H : Type*} [Group H] (f : G →* H) : ((G ⧸ f.ker) ≃* f.range) := by
  --have h : f.ker.Normal := inferInstance -- Serve?  No, perché è un'istanza di Group, non di GroupWithZero
  have h : f.ker ≤ f.ker := by
    exact le_rfl
    done
  set f' := QuotientGroup.lift f.ker f h with hf'
  have f'_range := MonoidHom.rangeRestrict_surjective f' -- Set.rangeFactorization f'
  have h' : f'.ker = ⊥ := by
    rw[eq_bot_iff_forall]
    intro x
    intro hx
    rw[MonoidHom.mem_ker] at hx
    have hp := QuotientGroup.mk'_surjective f.ker
    unfold Function.Surjective at hp
    rcases hp x with ⟨x', hx'⟩
    have : f x' = f' x := by
      rw[←hx']
      exact rfl
      done
    rw[hx] at this
    rw[← MonoidHom.mem_ker] at this
    have x'_in_ker : (QuotientGroup.mk' f.ker) x' = 1 := by
      rw [coe_mk']
      rw [eq_one_iff]
      exact this
      done
    rw[←hx',x'_in_ker]
    done
  rw[MonoidHom.ker_eq_bot_iff] at h'
  have h'' : f'.range = f.range := by
    ext y
    constructor
    -- sinistra -> destra
    intro hy
    rcases hy with ⟨x, hx⟩
    have hp' := QuotientGroup.mk'_surjective f.ker
    unfold Function.Surjective at hp'
    rcases hp' x with ⟨x', hx'⟩
    have : f x' = f' x := by
      rw[←hx']
      exact rfl
      done
    rw[hx] at this
    rw[MonoidHom.mem_range]
    use x'
    -- destra -> sinistra
    intro hy
    rcases hy with ⟨y', hy'⟩
    rw[MonoidHom.mem_range]
    use y'
    rw[←hy']
    exact rfl
    done
  rw[← h'']
  have f''_inj : (Function.Injective (MonoidHom.rangeRestrict f')) := MonoidHom.rangeRestrict_injective_iff.mpr h'
  have sp : Function.Surjective (MonoidHom.rangeRestrict f') := f'_range
  have f''_iso : Function.Bijective (MonoidHom.rangeRestrict f') := by
    exact ⟨f''_inj, sp⟩
  exact MulEquiv.ofBijective (MonoidHom.rangeRestrict f') f''_iso

As you see, everything is built around the lien set f' := QuotientGroup.lift f.ker f h with hf' and everything works perfectly. What I wanted to know is whether there is a way (although sub-optimal), and if yes how, to define without invoking any theorem f' as a group function from the quotient to the image and then proving that is well defined, and then using it as f' of theorem above (since set f' := QuotientGroup.lift f.ker f h with hf'already does all this work for me).
Any help or even tip about my code would be appreciated, thank you for your time.

[Martin Dvořák]

Imports are missing.

[brokkilisoup]

I'm sorry youre right, these are my imports

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.Perm.Subgroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.Subgroup.Basic

[Martin Dvořák]

I get "unknown identifier 'eq_bot_iff_forall'".

[Eric Wieser]

Please edit your importants into your previous message so that the "view in lean4 playground" link works!

[brokkilisoup]

Martin Dvořák ha scritto:

I get "unknown identifier 'eq_bot_iff_forall'".

I don't know why, could be that I have an update version of Lean or? eq_bot_iff_forall is not a lemma I added, with #check I get

Subgroup.eq_bot_iff_forall.{u_1} {G : Type u_1} [inst✝ : Group G] (H : Subgroup G) : H = ⊥ ↔ ∀ x ∈ H, x = 1

[brokkilisoup]

Eric Wieser ha scritto:

Please edit your importants into your previous message so that the "view in lean4 playground" link works!

Done, thank you for the tip

[Martin Dvořák]

Some superficial (i.e., without understanding the proof) refactoring for you (let diff be your code review):

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.Perm.Subgroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.Subgroup.Basic

open QuotientGroup

theorem first_isomorphism_theorem {G : Type*} [Group G] {H : Type*} [Group H] (f : G →* H) : ((G ⧸ f.ker) ≃* f.range) := by
  --have h : f.ker.Normal := inferInstance -- Serve?  No, perché è un'istanza di Group, non di GroupWithZero
  have h : f.ker ≤ f.ker := by
    rfl
  set f' := QuotientGroup.lift f.ker f h with hf'
  have f'_range := MonoidHom.rangeRestrict_surjective f' -- Set.rangeFactorization f'
  have h' : f'.ker = ⊥ := by
    sorry
  rw[MonoidHom.ker_eq_bot_iff] at h'
  have h'' : f'.range = f.range := by
    ext y
    constructor
    -- sinistra -> destra
    · intro hy
      rcases hy with ⟨x, hx⟩
      have hp' := QuotientGroup.mk'_surjective f.ker
      unfold Function.Surjective at hp'
      rcases hp' x with ⟨x', hx'⟩
      have : f x' = f' x := by
        rw[←hx']
        rfl
      rw[hx] at this
      rw[MonoidHom.mem_range]
      use x'
    -- destra -> sinistra
    · intro hy
      rcases hy with ⟨y', hy'⟩
      rw[MonoidHom.mem_range]
      use y'
      rw[←hy']
      rfl
  rw[← h'']
  have f''_inj : (Function.Injective (MonoidHom.rangeRestrict f')) := MonoidHom.rangeRestrict_injective_iff.mpr h'
  have f''_iso : Function.Bijective (MonoidHom.rangeRestrict f') := ⟨f''_inj, f'_range⟩
  exact MulEquiv.ofBijective (MonoidHom.rangeRestrict f') f''_iso

[brokkilisoup]

Martin Dvořák ha scritto:

Some superficial (i.e., without understanding the proof) refactoring for you (let diff be your code review):

import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.GroupTheory.Perm.Subgroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.Subgroup.Basic

open QuotientGroup

theorem first_isomorphism_theorem {G : Type*} [Group G] {H : Type*} [Group H] (f : G →* H) : ((G ⧸ f.ker) ≃* f.range) := by
  --have h : f.ker.Normal := inferInstance -- Serve?  No, perché è un'istanza di Group, non di GroupWithZero
  have h : f.ker ≤ f.ker := by
    rfl
  set f' := QuotientGroup.lift f.ker f h with hf'
  have f'_range := MonoidHom.rangeRestrict_surjective f' -- Set.rangeFactorization f'
  have h' : f'.ker = ⊥ := by
    sorry
  rw[MonoidHom.ker_eq_bot_iff] at h'
  have h'' : f'.range = f.range := by
    ext y
    constructor
    -- sinistra -> destra
    · intro hy
      rcases hy with ⟨x, hx⟩
      have hp' := QuotientGroup.mk'_surjective f.ker
      unfold Function.Surjective at hp'
      rcases hp' x with ⟨x', hx'⟩
      have : f x' = f' x := by
        rw[←hx']
        rfl
      rw[hx] at this
      rw[MonoidHom.mem_range]
      use x'
    -- destra -> sinistra
    · intro hy
      rcases hy with ⟨y', hy'⟩
      rw[MonoidHom.mem_range]
      use y'
      rw[←hy']
      rfl
  rw[← h'']
  have f''_inj : (Function.Injective (MonoidHom.rangeRestrict f')) := MonoidHom.rangeRestrict_injective_iff.mpr h'
  have f''_iso : Function.Bijective (MonoidHom.rangeRestrict f') := ⟨f''_inj, f'_range⟩
  exact MulEquiv.ofBijective (MonoidHom.rangeRestrict f') f''_iso

Thanks, however I was asking whether I could skip "lift" usage and defining f' myself, showing that is well defined

[Eric Wieser]

If you want to do it "from the basics" for pedagogical reasons, you can use Quotient.lift instead of QuotientGroup.lift