Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.IsIso f := by

Mathlib declaration: CategoryTheory.isIso_of_hom_simple
Held-out module: Mathlib.CategoryTheory.Preadditive.Schur
Banned modules (itself + downstream): 16
Reference proof premises (reachable / held-out): 1 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

No configuration has attempted this theorem yet.

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- The part of **Schur's lemma** that holds in any preadditive category with kernels:
that a nonzero morphism between simple objects is an isomorphism.
-/
theorem isIso_of_hom_simple
    [HasKernels C] {X Y : C} [Simple X] [Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : IsIso f :=
  haveI := mono_of_nonzero_from_simple w
  isIso_of_mono_of_nonzero w