Documentation Verification Report

Jointly

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

Statistics

Metric	Count
Definitions `JointlyFaithful`, `JointlyReflectEpimorphisms`, `JointlyReflectIsomorphisms`, `JointlyReflectMonomorphisms`	4
Theorems `jointlyReflectEpimorphisms`, `jointlyReflectMonomorphisms`, `jointlyReflectsIsomorphisms`, `map_injective`, `of_jointly_reflects_isIso_of_mono`, `epi`, `epi_iff`, `epi`, `isIso`, `isIso_iff`, `jointlyFaithful`, `jointlyReflectEpimorphisms`, `jointlyReflectMonomorphisms`, `mono`, `mono`, `mono_iff`	16
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
`JointlyFaithful` 📖	CompData	3 math math: `JointlyFaithful.of_jointly_reflects_isIso_of_mono`, `JointlyReflectIsomorphisms.jointlyFaithful`, `ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful`
`JointlyReflectEpimorphisms` 📖	CompData	3 math math: `JointlyFaithful.jointlyReflectEpimorphisms`, `JointlyReflectIsomorphisms.jointlyReflectEpimorphisms`, `ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms`
`JointlyReflectIsomorphisms` 📖	CompData	3 math math: `ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type`, `ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms`, `JointlyFaithful.jointlyReflectsIsomorphisms`
`JointlyReflectMonomorphisms` 📖	CompData	3 math math: `JointlyReflectIsomorphisms.jointlyReflectMonomorphisms`, `ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms`, `JointlyFaithful.jointlyReflectMonomorphisms`

CategoryTheory.JointlyFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jointlyReflectEpimorphisms` 📖	mathematical	`CategoryTheory.JointlyFaithful`	`CategoryTheory.JointlyReflectEpimorphisms`	—	`map_injective` `CategoryTheory.cancel_epi`
`jointlyReflectMonomorphisms` 📖	mathematical	`CategoryTheory.JointlyFaithful`	`CategoryTheory.JointlyReflectMonomorphisms`	—	`map_injective` `CategoryTheory.cancel_mono`
`jointlyReflectsIsomorphisms` 📖	mathematical	`CategoryTheory.JointlyFaithful`	`CategoryTheory.JointlyReflectIsomorphisms`	—	`CategoryTheory.JointlyReflectMonomorphisms.mono` `jointlyReflectMonomorphisms` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.JointlyReflectEpimorphisms.epi` `jointlyReflectEpimorphisms` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Balanced.isIso_of_mono_of_epi`
`map_injective` 📖	—	`CategoryTheory.JointlyFaithful` `CategoryTheory.Functor.map`	—	—	—
`of_jointly_reflects_isIso_of_mono` 📖	mathematical	`CategoryTheory.Limits.PreservesLimitsOfShape` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.IsIso`	`CategoryTheory.JointlyFaithful`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.equalizer.ι_mono` `CategoryTheory.Limits.equalizer.condition` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.Fork.IsLimit.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.eq_of_epi_equalizer` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso`

CategoryTheory.JointlyReflectEpimorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	`CategoryTheory.JointlyReflectEpimorphisms` `CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`CategoryTheory.Epi`	—	—
`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` 📖	mathematical	`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.Epi`	—	`CategoryTheory.Limits.pushout.condition` `CategoryTheory.epi_iff_isIso_inl` `isIso_iff`
`isIso` 📖	mathematical	`CategoryTheory.JointlyReflectIsomorphisms` `CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	`CategoryTheory.IsIso`	—	—
`isIso_iff` 📖	mathematical	`CategoryTheory.JointlyReflectIsomorphisms`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_isIso` `isIso`
`jointlyFaithful` 📖	mathematical	`CategoryTheory.JointlyReflectIsomorphisms` `CategoryTheory.Limits.PreservesLimitsOfShape` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory`	`CategoryTheory.JointlyFaithful`	—	`CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_mono` `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` 📖	mathematical	`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.Mono`	—	`CategoryTheory.Limits.pullback.condition` `CategoryTheory.mono_iff_isIso_fst` `isIso_iff`

CategoryTheory.JointlyReflectMonomorphisms

Theorems

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

---

← Back to Index