instDivisionRingEndOfHasKernelsOfSimple

Mathlib.CategoryTheory.Preadditive.Schur

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instDivisionRingEndOfHasKernelsOfSimple

Lean4

/-- In any preadditive category with kernels,
the endomorphisms of a simple object form a division ring. -/
noncomputable instance [HasKernels C] {X : C} [Simple X] : DivisionRing (End X)
    where
  inv
    f :=
    if h : f = 0 then 0
    else
      haveI := isIso_of_hom_simple h;
      inv f
  exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩
  inv_zero := dif_pos rfl
  mul_inv_cancel f
    hf := by
    dsimp
    rw [dif_neg hf]
    haveI := isIso_of_hom_simple hf
    exact IsIso.inv_hom_id f
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru