of_iso — Mathlib

English

If i: X ≅ Y and Y is simple, then X is simple.

Русский

Если i: X ≅ Y и Y простое, то X простое.

LaTeX

$$$ i: X \cong Y, [Simple\ Y] \Rightarrow Simple\ X. $$$

Lean4

theorem of_iso {X Y : C} [Simple Y] (i : X ≅ Y) : Simple X :=
  {
    mono_isIso_iff_nonzero := fun f m => by
      constructor
      · intro h w
        have j : IsIso (f ≫ i.hom) := by infer_instance
        rw [Simple.mono_isIso_iff_nonzero] at j
        subst w
        simp at j
      · intro h
        have j : IsIso (f ≫ i.hom) := by
          apply isIso_of_mono_of_nonzero
          intro w
          apply h
          simpa using (cancel_mono i.inv).2 w
        rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
        infer_instance }

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