Structures · Category theory
CategoryTheory.Simple
An object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero.
- Defined in
- Mathlib.CategoryTheory.Simple
- Shape
- One type argument · adds mono_isIso_iff_nonzero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- ModuleCat
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- CategoryTheory.Simple.mono_isIso_iff_nonzero
- CategoryTheory.isIso_of_mono_of_nonzero
- CategoryTheory.isIso_iff_nonzero
- CategoryTheory.id_nonzero
- CategoryTheory.Simple.of_iso
- CategoryTheory.finrank_hom_simple_simple_le_one
- CategoryTheory.Functor.simple_of_simple_obj
- CategoryTheory.isIso_of_epi_of_nonzero
- CategoryTheory.finrank_hom_simple_simple_eq_one_iff
- CategoryTheory.simple_obj
- CategoryTheory.finrank_endomorphism_simple_eq_one
- FDRep.char_orthonormal
- CategoryTheory.isIso_of_hom_simple
- CategoryTheory.finrank_hom_simple_simple_eq_zero_iff
- CategoryTheory.endomorphism_simple_eq_smul_id
- CategoryTheory.finrank_hom_simple_simple
- CategoryTheory.kernel_zero_of_nonzero_from_simple
- CategoryTheory.Simple.not_isZero
- FDRep.finrank_hom_simple_simple
- CategoryTheory.zero_not_simple
- CategoryTheory.instNontrivialEndOfSimple
- CategoryTheory.mono_of_nonzero_from_simple
- CategoryTheory.instIsSimpleOrderSubobjectOfSimple
- CategoryTheory.fieldEndOfFiniteDimensional
- CategoryTheory.mono_to_simple_zero_of_not_iso
- CategoryTheory.epi_of_nonzero_to_simple
- CategoryTheory.instNontrivialSubobjectOfSimple
- isSimpleModule_of_simple
- CategoryTheory.indecomposable_of_simple
- CategoryTheory.cokernel_zero_of_nonzero_to_simple
- CategoryTheory.instDivisionRingEndOfHasKernelsOfSimple
- CategoryTheory.epi_from_simple_zero_of_not_iso
- CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso
Ancestors0
No ancestors.