Documentation Verification Report

Concrete

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Concrete.lean

Statistics

Metric	Count
Definitions `FunctorialSurjectiveInjectiveFactorizationData`, `HasFunctorialSurjectiveInjectiveFactorization`, `HasSurjectiveInjectiveFactorization`, `bijective`, `injective`, `surjective`, `functorialSurjectiveInjectiveFactorizationData`	7
Theorems `bijective_eq_sup`, `bijective_respectsIso`, `injective_respectsIso`, `instIsMultiplicativeBijective`, `instIsMultiplicativeInjective`, `instIsMultiplicativeSurjective`, `surjective_respectsIso`, `instHasFunctorialSurjectiveInjectiveFactorizationTypeHom`	8
Total	15

CategoryTheory

Definitions

Name	Category	Theorems
`functorialSurjectiveInjectiveFactorizationData` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasFunctorialSurjectiveInjectiveFactorizationTypeHom` 📖	mathematical	—	`ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization` `types` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Types.instFunLike` `Types.instConcreteCategory`	—	—

CategoryTheory.ConcreteCategory

Definitions

Name	Category	Theorems
`FunctorialSurjectiveInjectiveFactorizationData` 📖	CompOp	—
`HasFunctorialSurjectiveInjectiveFactorization` 📖	MathDef	2 math math: `CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHom`, `instHasFunctorialSurjectiveInjectiveFactorization`
`HasSurjectiveInjectiveFactorization` 📖	MathDef	—

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`bijective` 📖	CompOp	3 math math: `instIsMultiplicativeBijective`, `bijective_respectsIso`, `bijective_eq_sup`
`injective` 📖	CompOp	6 math math: `CategoryTheory.ConcreteCategory.injective_eq_monomorphisms`, `CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff`, `bijective_eq_sup`, `injective_respectsIso`, `instIsMultiplicativeInjective`, `CategoryTheory.ConcreteCategory.injective_le_monomorphisms`
`surjective` 📖	CompOp	6 math math: `bijective_eq_sup`, `CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff`, `CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms`, `instIsMultiplicativeSurjective`, `surjective_respectsIso`, `CategoryTheory.ConcreteCategory.surjective_le_epimorphisms`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_eq_sup` 📖	mathematical	—	`bijective` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `injective` `surjective`	—	—
`bijective_respectsIso` 📖	mathematical	—	`RespectsIso` `bijective`	—	`respectsIso_of_isStableUnderComposition` `IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeBijective` `Equiv.bijective`
`injective_respectsIso` 📖	mathematical	—	`RespectsIso` `injective`	—	`respectsIso_of_isStableUnderComposition` `IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeInjective` `Equiv.injective`
`instIsMultiplicativeBijective` 📖	mathematical	—	`IsMultiplicative` `bijective`	—	`CategoryTheory.id_apply` `Function.bijective_id` `CategoryTheory.hom_comp` `Function.Bijective.comp`
`instIsMultiplicativeInjective` 📖	mathematical	—	`IsMultiplicative` `injective`	—	`CategoryTheory.id_apply` `CategoryTheory.hom_comp`
`instIsMultiplicativeSurjective` 📖	mathematical	—	`IsMultiplicative` `surjective`	—	`CategoryTheory.id_apply` `CategoryTheory.hom_comp`
`surjective_respectsIso` 📖	mathematical	—	`RespectsIso` `surjective`	—	`respectsIso_of_isStableUnderComposition` `IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeSurjective` `Equiv.surjective`

---

← Back to Index