Zulip Chat Archive

Stream: maths

Topic: quiz

Johan Commelin (Jul 12 2021 at 06:20):

Which well-known lemma in homological algebra is this:

lemma is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso : is_iso γ :=

@Markus Himmel is not allowed to participate in this quiz.

Johan Commelin (Jul 12 2021 at 06:21):

The following spoiler contains a hint, namely the proof. (It doesn't contain the answer. So feel free to take a look.)

have mono γ, by apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃; apply_instance,
have epi γ, by apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄; apply_instance,
by exactI is_iso_of_mono_of_epi _

Sebastien Gouezel (Jul 12 2021 at 06:48):

You have 5 isos in your statement, right?

Damiano Testa (Jul 12 2021 at 07:01):

Damiano Testa (Jul 12 2021 at 07:47):

The latest commit to master is a huge spoiler! :upside_down:

Last updated: Dec 20 2023 at 11:08 UTC