EpiMono

📁 Source: Mathlib/CategoryTheory/Limits/EpiMono.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_iff_inl_eq_inr, epi_iff_isIso_inl, epi_iff_isIso_inr, epi_iff_isPushout, mono_iff_fst_eq_snd, mono_iff_isIso_fst, mono_iff_isIso_snd, mono_iff_isPullback	8
Total	8

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_inl_eq_inr 📖	mathematical	—	Epi Limits.PushoutCocone.inl Limits.PushoutCocone.inr	—	cancel_epi Limits.PushoutCocone.condition
epi_iff_isIso_inl 📖	mathematical	—	Epi IsIso Limits.Cocone.pt Limits.WalkingSpan Limits.WidePushoutShape.category Limits.WalkingPair Limits.span Limits.PushoutCocone.inl	—	epi_iff_inl_eq_inr Category.comp_id Limits.PushoutCocone.IsColimit.hom_ext Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cancel_epi epi_of_strongEpi strongEpi_of_isIso cancel_mono IsSplitMono.mono
epi_iff_isIso_inr 📖	mathematical	—	Epi IsIso Limits.Cocone.pt Limits.WalkingSpan Limits.WidePushoutShape.category Limits.WalkingPair Limits.span Limits.PushoutCocone.inr	—	epi_iff_isIso_inl
epi_iff_isPushout 📖	mathematical	—	Epi IsPushout CategoryStruct.id Category.toCategoryStruct	—	IsPushout.of_isColimit epi_iff_inl_eq_inr
mono_iff_fst_eq_snd 📖	mathematical	—	Mono Limits.PullbackCone.fst Limits.PullbackCone.snd	—	cancel_mono Limits.PullbackCone.condition
mono_iff_isIso_fst 📖	mathematical	—	Mono IsIso Limits.Cone.pt Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair Limits.cospan Limits.PullbackCone.fst	—	mono_iff_fst_eq_snd Category.id_comp Limits.PullbackCone.IsLimit.hom_ext Category.assoc Category.comp_id cancel_mono mono_of_strongMono strongMono_of_isIso cancel_epi IsSplitEpi.epi
mono_iff_isIso_snd 📖	mathematical	—	Mono IsIso Limits.Cone.pt Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair Limits.cospan Limits.PullbackCone.snd	—	mono_iff_isIso_fst
mono_iff_isPullback 📖	mathematical	—	Mono IsPullback CategoryStruct.id Category.toCategoryStruct	—	IsPullback.of_isLimit mono_iff_fst_eq_snd

---

← Back to Index