kernelIsoKer — Mathlib

English

The categorical kernel inclusion for f : G ⟶ H, as an object over G, agrees with the AddCommGrpCat.ofHom (ker f).ker.subtype.

Русский

Каноническое включение ядра в виде объекта над G совпадает с AddCommGrpCat.ofHom (ker f).ker.subtype.

LaTeX

$$$\\text{kernelIsoKerOver}(f) : Over.mk(\\ker \\!f) \\cong Over.mk(\\mathrm{ofHom}(\\ker f))$$$

Lean4

/-- The categorical kernel of a morphism in `AddCommGrpCat`
agrees with the usual group-theoretical kernel.
-/
def kernelIsoKer {G H : AddCommGrpCat.{u}} (f : G ⟶ H) : kernel f ≅ AddCommGrpCat.of f.hom.ker
    where
  hom :=
    ofHom
      { toFun := fun g => ⟨kernel.ι f g, ConcreteCategory.congr_hom (kernel.condition f) g⟩
        map_zero' := by
          refine Subtype.ext ?_
          simp only [map_zero, ZeroMemClass.coe_zero]
        map_add' := fun g g' => by
          refine Subtype.ext ?_
          simp }
  inv := kernel.lift f (ofHom (AddSubgroup.subtype f.hom.ker)) <| by ext x; exact x.2
  hom_inv_id := by
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): it would be nice to do the next two steps by a single `ext`,
        -- but this will require thinking carefully about the relative priorities of `@[ext]` lemmas.

    refine equalizer.hom_ext ?_
    ext
    simp
  inv_hom_id := by
    apply AddCommGrpCat.ext
    rintro ⟨x, mem⟩
    refine Subtype.ext ?_
    apply ConcreteCategory.congr_hom (kernel.lift_ι f _ _)

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