Theorems · Definition · category theory
CategoryTheory.Types.jointlySurjectivePrecoverage
CategoryTheory.Precoverage (Type u)
The jointly surjective precoverage in the category of types has the jointly surjective families as coverings.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homproof · cited by 32,603
- Set.ofPredproof · cited by 6,101
- Set.rangeproof · cited by 4,705
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CategoryTheory.Presieveproof · cited by 449
- CategoryTheory.Precoveragestatement · cited by 204
Cited by12
Results whose statement or proof uses this declaration.
- TopCat.precoverageproof · cited by 3
- AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iffproof · cited by 2
- CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iffstatement and proof · cited by 1
- TopCat.exists_mem_zeroHypercover_rangeproof · cited by 1
- AlgebraicGeometry.Scheme.jointlySurjectivePrecoverageproof · cited by 1
- CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iffstatement · cited by 1
- CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iffstatement · cited by 0
- CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoveragestatement and proof · cited by 0
- AlgebraicGeometry.IsOpenImmersion.of_forall_source_existsproof · cited by 0
- CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iffstatement and proof · cited by 0
- CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iffstatement and proof · cited by 0
- TopCat.precoverage_le_comap_uliftFunctorproof · cited by 0