JointlySurjective

📁 Source: Mathlib/CategoryTheory/Sites/JointlySurjective.lean

Statistics

Metric	Count
Definitions JointlySurjective, jointlySurjectivePrecoverage	2
Theorems mem_comap_jointlySurjectivePrecoverage_iff, ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, instHasIsosJointlySurjectivePrecoverage, instIsStableUnderCompositionJointlySurjectivePrecoverage, instIsStableUnderSupJointlySurjectivePrecoverage, instSmallJointlySurjectivePrecoverage, mem_jointlySurjectivePrecoverage_iff, ofArrows_mem_jointlySurjectivePrecoverage_iff, singleton_mem_jointlySurjectivePrecoverage_iff, instIsStableUnderBaseChangeJointlySurjectivePrecoverage, isStableUnderBaseChange_comap_jointlySurjectivePrecoverage	11
Total	13

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
JointlySurjective 📖	CompData	1 math math: instJointlySurjectivePrecoverage

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStableUnderBaseChangeJointlySurjectivePrecoverage 📖	mathematical	—	Precoverage.IsStableUnderBaseChange types Types.jointlySurjectivePrecoverage	—	Precoverage.comap_id isStableUnderBaseChange_comap_jointlySurjectivePrecoverage surjective_of_epi Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self epi_of_strongEpi strongEpi_of_isIso Limits.instIsIsoPullbackComparison Functor.corepresentable_preservesLimit instIsCorepresentableIdType
isStableUnderBaseChange_comap_jointlySurjectivePrecoverage 📖	mathematical	Functor.obj types Limits.pullback Functor.map Limits.Types.hasLimit Limits.WalkingCospan Limits.WidePullbackShape.category Limits.WalkingPair UnivLE.small univLE_of_max UnivLE.self Limits.cospan Limits.pullbackComparison	Precoverage.IsStableUnderBaseChange Precoverage.comap Types.jointlySurjectivePrecoverage	—	Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self Precoverage.mem_comap_iff Presieve.map_ofArrows Types.ofArrows_mem_jointlySurjectivePrecoverage_iff IsPullback.hasPullback Limits.pullbackComparison_comp_fst IsPullback.isoPullback_hom_fst types_comp Function.comp_assoc Set.range_comp Function.Surjective.range_eq surjective_of_epi epi_of_strongEpi strongEpi_of_isIso Functor.map_isIso Iso.isIso_hom Set.image_univ Limits.Types.range_pullbackFst

CategoryTheory.Presieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_comap_jointlySurjectivePrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Precoverage.comap CategoryTheory.types CategoryTheory.Types.jointlySurjectivePrecoverage CategoryTheory.Functor.obj Set.range CategoryTheory.Functor.map	—	CategoryTheory.Precoverage.mem_comap_iff
ofArrows_mem_comap_jointlySurjectivePrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Precoverage.comap CategoryTheory.types CategoryTheory.Types.jointlySurjectivePrecoverage ofArrows CategoryTheory.Functor.obj Set.range CategoryTheory.Functor.map	—	map_ofArrows

CategoryTheory.Types

Definitions

Name	Category	Theorems
jointlySurjectivePrecoverage 📖	CompOp	11 math math: CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage, mem_jointlySurjectivePrecoverage_iff, CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, singleton_mem_jointlySurjectivePrecoverage_iff, CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage, CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff, instIsStableUnderCompositionJointlySurjectivePrecoverage, instSmallJointlySurjectivePrecoverage, instHasIsosJointlySurjectivePrecoverage, instIsStableUnderSupJointlySurjectivePrecoverage, ofArrows_mem_jointlySurjectivePrecoverage_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasIsosJointlySurjectivePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.HasIsos CategoryTheory.types jointlySurjectivePrecoverage	—	CategoryTheory.surjective_of_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso
instIsStableUnderCompositionJointlySurjectivePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderComposition CategoryTheory.types jointlySurjectivePrecoverage	—	—
instIsStableUnderSupJointlySurjectivePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.IsStableUnderSup CategoryTheory.types jointlySurjectivePrecoverage	—	—
instSmallJointlySurjectivePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.Small CategoryTheory.types jointlySurjectivePrecoverage	—	ofArrows_mem_jointlySurjectivePrecoverage_iff CategoryTheory.Precoverage.ZeroHypercover.mem₀
mem_jointlySurjectivePrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve CategoryTheory.types Set Set.instMembership CategoryTheory.Precoverage.coverings jointlySurjectivePrecoverage Set.range	—	—
ofArrows_mem_jointlySurjectivePrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve CategoryTheory.types Set Set.instMembership CategoryTheory.Precoverage.coverings jointlySurjectivePrecoverage CategoryTheory.Presieve.ofArrows Set.range	—	—
singleton_mem_jointlySurjectivePrecoverage_iff 📖	mathematical	—	CategoryTheory.Presieve CategoryTheory.types Set Set.instMembership CategoryTheory.Precoverage.coverings jointlySurjectivePrecoverage CategoryTheory.Presieve.singleton	—	mem_jointlySurjectivePrecoverage_iff Function.Surjective.range_eq

---

← Back to Index