isoModSerre_kernel_eq_inverseImage_isomorphisms

English

For morphism g, the kernel isomorphism equals the inverse image under G of the isomorphisms on C.

Русский

Морфизм g имеет изоморфизм ядра, равный образу обратного изображения по G из изоморфизмов на C.

LaTeX

$$G.kernel.isoModSerre = (isomorphisms C).inverseImage G$$

Lean4

theorem isoModSerre_kernel_eq_inverseImage_isomorphisms : G.kernel.isoModSerre = (isomorphisms C).inverseImage G :=
  by
  ext X Y f
  refine ⟨(G.kernel.isoModSerre_isInvertedBy_iff G).2 (by rfl) _, fun hf ↦ ?_⟩
  simp only [inverseImage_iff, isomorphisms.iff] at hf
  constructor
  · exact KernelFork.IsLimit.isZero_of_mono (KernelFork.mapIsLimit _ (kernelIsKernel f) G)
  · exact CokernelCofork.IsColimit.isZero_of_epi (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

Похожие утверждения