Lemma Using First Isomorphism Theorem

Stream: Is there code for X?

[brokkilisoup]

Hello, I'm a master student (new in Lean) trying to Re-proving First Isomorphism Theorem and some corollaries. I managed to give a proof of the First Isomorphism Theorem using the "lift" function and now I'm trying to do an exercise using it. In particular, the following

lemma ProdCylic {G : Type*} [Group G] {H K : Subgroup G} [H.Normal] [K.Normal] (h : Disjoint H K) (p: ℕ) (hp : Nat.Prime p) (h1 : H.index = p) (h2 : K.index = p) : G ≃* (G ⧸ H) × (G ⧸ K) := by
 let f : G →* (G ⧸ H) × (G ⧸ K) := (QuotientGroup.mk' H).prod (QuotientGroup.mk' K)
 have fSurj : Function.Surjective f := by
  sorry
 have KerCap : f.ker = H ⊓ K := by
  rw[MonoidHom.ker_prod]
  rw[QuotientGroup.ker_mk',QuotientGroup.ker_mk']
  done
 have KerCapBot : f.ker = ⊥ := by
    rw[KerCap]
    exact h.eq_bot
    done
 have fImage : f.range = ((G ⧸ H) × (G ⧸ K)) := by
  rw[← MonoidHom.range_top_iff_surjective] at fSurj
  rw[eq_top_iff] at fSurj
  sorry
 have FirstIso := first_isomorphism_theorem f
 have KerTrivial := (QuotientGroup.quotientMulEquivOfEq KerCapBot).symm
 have GBot : G ≃* G ⧸ ⊥ := by
  exact QuotientGroup.quotientBot.symm
  done
 have concatenation : G ≃* G⧸MonoidHom.ker f := by
  exact MulEquiv.trans GBot KerTrivial
  done
 have finalIso : G ≃* MonoidHom.range f := by
  exact MulEquiv.trans concatenation FirstIso
  done
 have fImageIso : f.range ≃* ((G ⧸ H) × (G ⧸ K)) := by
  sorry
 have finalIso : G ≃* ((G ⧸ H) × (G ⧸ K)) := by
  exact MulEquiv.trans finalIso fImageIso
  done
 exact finalIso

In particular I got stucked in proving f.range = ((G ⧸ H) × (G ⧸ K)) because I'd like to find a theorem which gives that the product of projection has image the product of images (since for ker it exists). But I was unable to find it with moogle.ai or such. So I thought it could have been a good idea proving that f is surjective and then unfold who the codomain is, but I failed since I got problem in understanding how to use \top to my purpose.

Finally, the other theorem I'd like to know the name that I'm not finding is the one giving f.range ≃* ((G ⧸ H) × (G ⧸ K)) since I should have proved f.range = ((G ⧸ H) × (G ⧸ K)).

Any help would be appreciated as any other tip about the code as well, thank you for your time.

[Patrick Massot]

(deleted)

[Patrick Massot]

(deleted)

[Patrick Massot]

@brokkilisoup I don't have time to read your question in details, but did you do the very similar exercise from #mil?

[Patrick Massot]

The exercise is at the end of Section 8.1 and decomposed into several statements.

[brokkilisoup]

Patrick Massot ha scritto:

The exercise is at the end of Section 8.1 and decomposed into several statements.

Yes Indeed, and I managed to solve it. Here I didn't want to use the Theorem strictly related to first isomorphism theorem in mil since I made my own proof of first isomorphism theorem for exercise, and I was trying to use it to re-solve this corollary. But I got stucked here since I can't find the names for the theorems I'd like to apply.

[Thomas Browning]

Well, one thing that might help for this particular exercise is use docs#Subgroup.index_inf_le to show that G is actually finite with order p^2, and from there show that H and K satisfy docs#Subgroup.IsComplement'.