Prove the five lemma for groups #46
Loading…
Reference in a new issue
No description provided.
Delete branch "%!s()"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Update: Solution at
90f76baca0/src/Misc/FiveLemma/Group/Lemma.agda
Very close to the n surjective result, I defined a different definition of
isInIm
that isn't truncated:isInIm' : GroupHom G H → ⟨ H ⟩ → Type _
isInIm' {G = G} ϕ h = Σ[ g ∈ ⟨ G ⟩ ] ϕ .fst g ≡ h
Prove the five lemmato Prove the five lemma for groupsChanging this issue to specifically be about groups, will add another one for categories later
Done! See
90f76baca0/src/Misc/FiveLemma/Group/Lemma.agda
for solution