Jointly

📁 Source: Mathlib/CategoryTheory/Functor/ReflectsIso/Jointly.lean

Statistics

Metric	Count
Definitions JointlyReflectEpimorphisms, JointlyReflectIsomorphisms, JointlyReflectMonomorphisms	3
Theorems epi, epi_iff, epi, isIso, isIso_iff, jointlyReflectEpimorphisms, jointlyReflectMonomorphisms, mono, mono, mono_iff	10
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
JointlyReflectEpimorphisms 📖	CompData	1 math math: JointlyReflectIsomorphisms.jointlyReflectEpimorphisms
JointlyReflectIsomorphisms 📖	CompData	—
JointlyReflectMonomorphisms 📖	CompData	1 math math: JointlyReflectIsomorphisms.jointlyReflectMonomorphisms

CategoryTheory.JointlyReflectEpimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	—	CategoryTheory.JointlyReflectEpimorphisms CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	—
epi_iff 📖	mathematical	CategoryTheory.JointlyReflectEpimorphisms CategoryTheory.Functor.PreservesEpimorphisms	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_epi epi

CategoryTheory.JointlyReflectIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi 📖	—	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span	—	—	CategoryTheory.Limits.pushout.condition CategoryTheory.epi_iff_isIso_inl isIso_iff
isIso 📖	—	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	—
isIso_iff 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_isIso isIso
jointlyReflectEpimorphisms 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair	CategoryTheory.JointlyReflectEpimorphisms	—	epi CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
jointlyReflectMonomorphisms 📖	mathematical	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair	CategoryTheory.JointlyReflectMonomorphisms	—	mono CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
mono 📖	—	CategoryTheory.JointlyReflectIsomorphisms CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	—	CategoryTheory.Limits.pullback.condition CategoryTheory.mono_iff_isIso_fst isIso_iff

CategoryTheory.JointlyReflectMonomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	CategoryTheory.JointlyReflectMonomorphisms CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	—
mono_iff 📖	mathematical	CategoryTheory.JointlyReflectMonomorphisms CategoryTheory.Functor.PreservesMonomorphisms	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_mono mono

---

← Back to Index