!4#3510 CategoryTheory.Simple

Stream: mathlib4

[Jeremy Tan]

!4#3510 Two errors remain in this file:

theorem indecomposable_of_simple (X : C) [Simple X] : Indecomposable X :=
  ⟨Simple.not_isZero X, fun Y Z i => by
    refine' or_iff_not_imp_left.mpr fun h => _
    rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
    change biprod.inl ≠ 0 at h
    rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h -- here
    · rwa [biprod.is_iso_inl_iff_is_zero] at h
    · exact simple.of_iso i.symm
    · infer_instance⟩

Simple.lean:214:10
failed to synthesize instance
  Simple (?m.27073 ⊞ ?m.27074)
Simple.lean:214:8
tactic 'rewrite' failed, equality or iff proof expected
  ?m.28551
C: Type u
inst✝³: Category C
inst✝²: Preadditive C
inst✝¹: HasBinaryBiproducts C
X: C
inst✝: Simple X
YZ: C
i: X ≅ Y ⊞ Z
h: biprod.inl ≠ 0
⊢ IsZero Z

how do I fix them? ( doesn't work)

[Jeremy Tan]

(.)

[Jürgen Bergmann]

@Jeremy Tan This seems to work:

theorem indecomposable_of_simple (X : C) [Simple X] : Indecomposable X :=
  ⟨Simple.not_isZero X, fun Y Z i => by
    refine' or_iff_not_imp_left.mpr fun h => _
    rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
    change biprod.inl ≠ 0 at h
    have : Simple (Y ⊞ Z) := by exact Simple.of_iso i.symm
    rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
    rwa [Biprod.isIso_inl_iff_isZero] at h⟩

[Jeremy Tan]

@Jürgen Bergmann I already committed that fix, thanks