| Name | Category | Theorems |
|---|
WalkingCospan 📖 | CompOp | 366 mathmath: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.StructuredArrow.projectSubobject_mk, CategoryTheory.Over.μ_pullback_left_snd', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', TopCat.pullbackIsoProdSubtype_hom_fst, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl', CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, diagramIsoCospan_inv_app, diagonalObjPullbackFstIso_inv_snd_snd_assoc, walkingSpanOpEquiv_inverse_map, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', pullbackDiagonalMapIso.hom_fst, diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, pullbackFstFstIso_hom, prodIsoPullback_inv_fst, pullbackConeOfLeftIso_π_app_left, CategoryTheory.Abelian.epi_pullback_of_epi_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization, FormalCoproduct.homPullbackEquiv_symm_apply_φ, CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve, Types.range_pullbackFst, cospanExt_app_one, CategoryTheory.Over.monObjMkPullbackSnd_mul, diagonalObjPullbackFstIso_inv_fst_fst, TopCat.snd_isOpenEmbedding_of_left, PullbackCone.π_app_right, PushoutCocone.unop_π_app, CategoryTheory.Over.grpObjMkPullbackSnd_one, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', CategoryTheory.Over.grpObjMkPullbackSnd_mul, FormalCoproduct.pullbackCone_fst_φ, PullbackCone.condition, Types.pullbackIsoPullback_hom_fst, CategoryTheory.IsPullback.isLimit', pullbackDiagonalMapIso.inv_fst_assoc, pullback_diagonal_map_snd_snd_fst_assoc, diagonalObjPullbackFstIso_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, CompHausLike.pullback.isLimit_lift, PullbackCone.unop_inl, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, TopCat.pullback_topology, PullbackCone.mk_π_app, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, PullbackCone.IsLimit.lift_fst, prodIsoPullback_inv_fst_assoc, PullbackCone.op_pt, equalizerPullbackMapIso_inv_ι_snd, pullbackConeOfLeftIso_π_app_right, diagonalObjPullbackFstIso_inv_snd_fst, pullbackObjIso_inv_comp_fst_assoc, PullbackCone.IsLimit.equivPullbackObj_apply_fst, equalizerPullbackMapIso_inv_ι_fst, pullbackConeOfLeftIso_snd, walkingCospanOpEquiv_counitIso_hom_app, diagonalObjPullbackFstIso_hom_fst_fst_assoc, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, PullbackCone.condition_assoc, CategoryTheory.Over.preservesTerminalIso_pullback, PullbackCone.unop_inr, spanOp_hom_app, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, TopCat.fst_iso_of_right_embedding_range_subset, PullbackCone.combine_π_app, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks, equalizerPullbackMapIso_hom_fst_assoc, pullback.comp_diagonal_assoc, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, pullbackConeEquivBinaryFan_functor_map_hom, PullbackCone.op_inr, prodIsoPullback_hom_fst_assoc, walkingCospanOpEquiv_counitIso_inv_app, AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, PullbackCone.op_ι_app, pullbackConeEquivBinaryFan_counitIso, pullback_diagonal_map_snd_fst_fst, diagramIsoCospan_hom_app, diagonalObjPullbackFstIso_inv_snd_snd, IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, cospan_left, walkingCospanOpEquiv_inverse_obj, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, walkingSpanOpEquiv_inverse_obj, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map, cospanExt_app_right, TopCat.range_pullback_map, CategoryTheory.Subobject.pullback_obj, pullback_lift_diagonal_isPullback, walkingCospanOpEquiv_unitIso_inv_app, PullbackCone.mono_fst_of_is_pullback_of_mono, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, cospan_map_inr, cospanCompIso_inv_app_left, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, Cone.ofPullbackCone_pt, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion, spanOp_inv_app, cospan_map_inl, CategoryTheory.Over.tensorHom_left_snd_assoc, PullbackCone.isIso_fst_of_mono_of_isLimit, Types.pullbackLimitCone_cone, Cone.ofPullbackCone_π, pullbackConeOfRightIso_π_app_right, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, PullbackCone.snd_limit_cone, PullbackCone.mk_π_app_right, opSpan_hom_app, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', pullbackConeOfRightIso_fst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, pullbackConeOfRightIso_x, PullbackCone.mk_π_app_one, TopCat.Sheaf.interUnionPullbackConeLift_right, preservesPullback_symmetry, hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair, CategoryTheory.IsPullback.of_isLimit, TopCat.fst_isEmbedding_of_right, isPullback_map_snd_snd, pullbackConeEquivBinaryFan_inverse_obj, pullbackConeEquivBinaryFan_functor_obj, walkingSpanOpEquiv_counitIso_hom_app, CategoryTheory.Abelian.epi_snd_of_isLimit, TopCat.isOpenEmbedding_of_pullback, opCospan_hom_app, PullbackCone.IsLimit.equivPullbackObj_apply_snd, Types.pullbackIsoPullback_inv_snd, PullbackCone.π_app_left, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Square.isPullback_iff, TopCat.pullbackIsoProdSubtype_inv_snd_apply, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, TopCat.pullbackIsoProdSubtype_inv_fst, cospanCompIso_inv_app_right, FormalCoproduct.homPullbackEquiv_symm_apply_f_coe, PullbackCone.eta_inv_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, diagonalObjPullbackFstIso_inv_snd_fst_assoc, PushoutCocone.op_π_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, CategoryTheory.Over.closedUnderLimitsOfShape_pullback, walkingSpanOpEquiv_unitIso_inv_app, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl, opCospan_inv_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, TopCat.pullbackIsoProdSubtype_hom_snd, cospanExt_inv_app_one, PullbackCone.unop_ι_app, Types.pullbackIsoPullback_hom_snd, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, pullbackDiagonalMapIso.hom_snd, pullbackConeOfLeftIso_π_app_none, CategoryTheory.Over.μ_pullback_left_fst_fst', TopCat.snd_iso_of_left_embedding_range_subset, pullbackObjIso_hom_comp_fst, cospanOp_hom_app, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.monObjMkPullbackSnd_one, TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, PullbackCone.isoMk_inv_hom, pullback_diagonal_map_snd_fst_fst_assoc, PreservesPullback.of_iso_comparison, pullbackDiagonalMapIso.inv_snd_fst, prodIsoPullback_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, CategoryTheory.Regular.instHasCoequalizerFstSnd, cospan_right, cospanExt_app_left, TopCat.range_pullback_to_prod, TopCat.Sheaf.interUnionPullbackConeLift_left, PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, TopCat.pullback_fst_image_snd_preimage, CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, CompleteLattice.pullback_eq_inf, CategoryTheory.Abelian.epi_pullback_of_epi_g, prodIsoPullback_hom_snd_assoc, pullbackConeOfRightIso_π_app_left, pullbackConeOfLeftIso_x, walkingCospanOpEquiv_functor_map, CompHausLike.pullback.cone_π, TopCat.pullbackIsoProdSubtype_inv_fst_apply, pullbackObjIso_hom_comp_fst_assoc, CategoryTheory.Over.tensorHom_left_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, equalizerPullbackMapIso_hom_snd_assoc, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso, pullback.comp_diagonal, cospanExt_hom_app_one, cospan_map_id, walkingCospanOpEquiv_functor_obj, CategoryTheory.Over.tensorHom_left_fst_assoc, prodIsoPullback_hom_fst, walkingSpanOpEquiv_functor_map, PullbackCone.eta_hom_hom, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, CategoryTheory.Over.η_pullback_left, PullbackCone.mk_pt, cospanCompIso_inv_app_one, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, PullbackCone.ofCone_π, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, pullbackObjIso_inv_comp_fst, PullbackCone.op_inl, PullbackCone.IsLimit.lift_snd, equalizerPullbackMapIso_hom_snd, diagonalObjPullbackFstIso_hom_fst_snd, PullbackCone.flip_pt, Types.pullbackIsoPullback_inv_fst, Types.pullbackIsoPullback_inv_fst_apply, cospanCompIso_hom_app_left, equalizerPullbackMapIso_hom_fst, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.MonoOver.pullback_obj_left, TopCat.pullbackIsoProdSubtype_hom_apply, CoproductDisjoint.nonempty_isInitial_of_ne, pullbackDiagonalMapIso.inv_snd_fst_assoc, equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, FormalCoproduct.pullbackCone_fst_f, pullback.diagonal_comp, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', pullbackObjIso_hom_comp_snd_assoc, CategoryTheory.MorphismProperty.diagonal_iff, Types.range_pullbackSnd, CompHausLike.instHasLimitWalkingCospanCospan, TopCat.fst_isOpenEmbedding_of_right, cospanCompIso_hom_app_one, pullback_diagonal_map_snd_snd_fst, prodIsoPullback_inv_snd, PullbackCone.combine_pt_map, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, CategoryTheory.NormalMonoCategory.pullback_of_mono, PullbackCone.unop_pt, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, diagonalObjPullbackFstIso_inv_fst_fst_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight, PullbackCone.combine_pt_obj, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, PushoutCocone.op_pt, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, FormalCoproduct.pullbackCone_condition, CategoryTheory.regularTopology.equalizerCondition_w, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion, pullbackConeOfRightIso_π_app_none, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.Over.μ_pullback_left_snd, Types.pullbackLimitCone_isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, diagonalObjPullbackFstIso_hom_fst_snd_assoc, cospanExt_inv_app_left, PullbackCone.condition_one, CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit, pullbackObjIso_inv_comp_snd_assoc, pullbackDiagonalMapIso.inv_snd_snd_assoc, TopCat.pullback_map_isEmbedding, diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, cospanOp_inv_app, cospanCompIso_hom_app_right, diagonalObjPullbackFstIso_hom_fst_fst, pullbackDiagonalMapIso.hom_fst_assoc, PullbackCone.isIso_snd_of_mono_of_isLimit, cospanCompIso_app_one, walkingSpanOpEquiv_functor_obj, CategoryTheory.Abelian.epi_fst_of_isLimit, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong, CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1, PullbackCone.IsLimit.lift_fst_assoc, cospanCompIso_app_left, CategoryTheory.Over.tensorHom_left_snd, PushoutCocone.unop_pt, CategoryTheory.Presieve.uncurry_pullbackArrows, prodIsoPullback_inv_snd_assoc, walkingSpanOpEquiv_unitIso_hom_app, CategoryTheory.Over.lift_left, PullbackCone.IsLimit.lift_snd_assoc, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, PullbackCone.isoMk_hom_hom, pullback_map_eq_pullbackFstFstIso_inv, WalkingCospan.instSubsingletonHom, walkingSpanOpEquiv_counitIso_inv_app, CategoryTheory.mono_iff_isIso_fst, AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective, PullbackCone.ofCone_pt, PullbackCone.mk_π_app_left, diagonalObjPullbackFstIso_inv_fst_snd, FormalCoproduct.homPullbackEquiv_apply_coe, pullbackConeEquivBinaryFan_unitIso, CategoryTheory.Over.isMonHom_pullbackFst_id_right, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.Over.tensorObj_left, CategoryTheory.mono_iff_isIso_snd, equalizerPullbackMapIso_inv_ι_fst_assoc, Types.pullbackIsoPullback_inv_snd_apply, PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd, walkingCospanOpEquiv_unitIso_hom_app, PullbackCone.mono_snd_of_is_pullback_of_mono, TopCat.pullback_snd_range, opSpan_inv_app, CategoryTheory.IsPullback.of_isLimit_cone, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', TopCat.snd_isEmbedding_of_left, pullbackObjIso_inv_comp_snd, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, cospanExt_inv_app_right, CategoryTheory.Over.ε_pullback_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, pullback_fst_map_snd_isPullback, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, cospanExt_hom_app_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', pullbackDiagonalMapIso.inv_snd_snd, pullbackFstFstIso_inv, SSet.instFinitePullback, TopCat.pullback_fst_range, cospanExt_hom_app_left, FormalCoproduct.pullbackCone_snd_f, cospan_one, diagonal_pullback_fst, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, TopCat.pullback_snd_image_fst_preimage, pullback_lift_map_isPullback, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, FormalCoproduct.pullbackCone_snd_φ, walkingCospanOpEquiv_inverse_map, CategoryTheory.Over.tensorObj_hom, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, FormalCoproduct.isPullback, cospanCompIso_app_right, pullbackConeEquivBinaryFan_inverse_map_hom, CompHausLike.pullback.cone_pt, PullbackCone.fst_limit_cone, pullbackObjIso_hom_comp_snd, TopCat.isEmbedding_of_pullback, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, pullback_equalizer, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, CategoryTheory.Regular.instMonoDesc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right
|
WalkingSpan 📖 | CompOp | 180 mathmath: spanCompIso_app_left, pushoutCoconeOfLeftIso_ι_app_right, PushoutCocone.flip_pt, walkingSpanOpEquiv_inverse_map, CommRingCat.pushoutCocone_pt, spanCompIso_inv_app_zero, PushoutCocone.mk_ι_app_zero, PushoutCocone.inl_colimit_cocone, inl_coprodIsoPushout_hom, PushoutCocone.unop_π_app, inl_comp_pushoutObjIso_hom, pushoutCoconeEquivBinaryCofan_inverse_obj, pushoutCoconeEquivBinaryCofan_functor_obj, pushoutCoconeEquivBinaryCofan_unitIso, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, PushoutCocone.condition_assoc, span_map_id, PushoutCocone.op_snd, PushoutCocone.isoMk_inv_hom, PullbackCone.op_pt, span_right, inr_comp_pushoutObjIso_hom_assoc, PushoutCocone.epi_inl_of_is_pushout_of_epi, CategoryTheory.IsPushout.isColimit', pushoutCoconeEquivBinaryCofan_inverse_map_hom, walkingCospanOpEquiv_counitIso_hom_app, CommRingCat.Under.preservesFiniteLimits_of_flat, hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, spanCompIso_hom_app_zero, PushoutCocone.condition, spanOp_hom_app, CategoryTheory.Under.postAdjunctionRight_unit_app_right, spanExt_hom_app_right, spanCompIso_inv_app_left, Types.instMonoPushoutInl, walkingCospanOpEquiv_counitIso_inv_app, PullbackCone.op_ι_app, span_map_snd, walkingCospanOpEquiv_inverse_obj, walkingSpanOpEquiv_inverse_obj, walkingCospanOpEquiv_unitIso_inv_app, spanCompIso_app_zero, PushoutCocone.ofCocone_ι, spanExt_hom_app_zero, CommRingCat.HomTopology.isEmbedding_pushout, spanOp_inv_app, PushoutCocone.eta_inv_hom, inr_coprodIsoPushout_hom_assoc, opSpan_hom_app, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, spanCompIso_app_right, pushoutCoconeOfRightIso_x, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, PushoutCocone.condition_zero, PushoutCocone.ι_app_left, pushoutCoconeOfLeftIso_ι_app_left, PushoutCocone.ofCocone_pt, walkingSpanOpEquiv_counitIso_hom_app, spanExt_app_one, opCospan_hom_app, PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.SmallObject.ιFunctorObj_eq, CommRingCat.inr_injective_of_flat, spanCompIso_inv_app_right, PushoutCocone.mk_ι_app, PushoutCocone.ι_app_right, CategoryTheory.Abelian.mono_pushout_of_mono_g, spanExt_inv_app_zero, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, spanExt_app_left, CategoryTheory.BicartesianSq.isColimit', pushoutCoconeEquivBinaryCofan_functor_map_hom, PushoutCocone.IsColimit.inl_desc_assoc, PushoutCocone.inr_colimit_cocone, PushoutCocone.op_π_app, CompleteLattice.pushout_eq_sup, walkingSpanOpEquiv_unitIso_inv_app, opCospan_inv_app, PullbackCone.unop_ι_app, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, cospanOp_hom_app, AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, pushoutCoconeOfRightIso_ι_app_left, spanCompIso_hom_app_right, AlgebraicGeometry.isPullback_Spec_map_pushout, walkingCospanOpEquiv_functor_map, Types.pushoutCocone_inr_mono_of_isColimit, AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan, walkingCospanOpEquiv_functor_obj, walkingSpanOpEquiv_functor_map, PushoutCocone.mk_pt, PushoutCocone.IsColimit.inr_desc_assoc, CommRingCat.inl_injective_of_flat, pushoutCoconeOfLeftIso_ι_app_none, PushoutCocone.IsColimit.inr_desc, spanCompIso_hom_app_left, CategoryTheory.SmallObject.πFunctorObj_eq, inl_comp_pushoutObjIso_inv, PushoutCocone.epi_inr_of_is_pushout_of_epi, inr_comp_pushoutObjIso_inv, spanExt_hom_app_left, CommRingCat.tensorProdIsoPushout_app, CategoryTheory.Square.isPushout_iff, Cocone.ofPushoutCocone_ι, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, inl_comp_pushoutObjIso_inv_assoc, IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.MorphismProperty.ind_underObj_pushout, inr_coprodIsoPushout_hom, PushoutCocone.IsColimit.inl_desc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Abelian.mono_inl_of_isColimit, PullbackCone.unop_pt, span_map_fst, pushoutCoconeOfLeftIso_x, PushoutCocone.op_pt, PushoutCocone.mk_ι_app_right, span_left, inl_comp_pushoutObjIso_hom_assoc, AlgebraicGeometry.isPullback_SpecMap_pushout, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, inl_coprodIsoPushout_inv, AlgebraicGeometry.isIso_pushoutSection_iff, PreservesPushout.of_iso_comparison, PushoutCocone.isoMk_hom_hom, cospanOp_inv_app, pushoutCoconeOfRightIso_ι_app_none, PushoutCocone.mk_ι_app_left, walkingSpanOpEquiv_functor_obj, CategoryTheory.Abelian.mono_pushout_of_mono_f, Types.Pushout.cocone_ι_app, CategoryTheory.epi_iff_isIso_inl, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, inr_coprodIsoPushout_inv, PushoutCocone.unop_pt, PushoutCocone.eta_hom_hom, spanExt_app_right, walkingSpanOpEquiv_unitIso_hom_app, inl_coprodIsoPushout_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, pushoutCoconeEquivBinaryCofan_counitIso, inr_comp_pushoutObjIso_inv_assoc, Types.instMonoPushoutInr, inr_comp_pushoutObjIso_hom, CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization, CategoryTheory.Abelian.mono_inr_of_isColimit, diagramIsoSpan_inv_app, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, CategoryTheory.IsPushout.of_isColimit, span_zero, walkingSpanOpEquiv_counitIso_inv_app, preservesPushout_symmetry, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, Cocone.ofPushoutCocone_pt, WalkingSpan.instSubsingletonHom, inl_coprodIsoPushout_inv_assoc, walkingCospanOpEquiv_unitIso_hom_app, opSpan_inv_app, PushoutCocone.isIso_inr_of_epi_of_isColimit, pushoutCoconeOfRightIso_ι_app_right, CategoryTheory.NormalEpiCategory.pushout_of_epi, inr_coprodIsoPushout_inv_assoc, PushoutCocone.unop_snd, CategoryTheory.epi_iff_isIso_inr, diagramIsoSpan_hom_app, CategoryTheory.CostructuredArrow.projectQuotient_mk, PushoutCocone.unop_fst, CategoryTheory.IsPushout.of_isColimit_cocone, PushoutCocone.op_fst, Types.pushoutCocone_inr_injective_of_isColimit, spanExt_inv_app_right, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, RingHom.IsStableUnderBaseChange.pushout_inl, walkingCospanOpEquiv_inverse_map, spanExt_inv_app_left, Types.Pushout.cocone_pt, CategoryTheory.IsPushout.isVanKampen_iff, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
|
cospan 📖 | CompOp | 345 mathmath: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.Over.μ_pullback_left_snd', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right', TopCat.pullbackIsoProdSubtype_hom_fst, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl', CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, diagramIsoCospan_inv_app, diagonalObjPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right', pullbackDiagonalMapIso.hom_fst, diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, pullbackFstFstIso_hom, prodIsoPullback_inv_fst, pullbackConeOfLeftIso_π_app_left, CategoryTheory.Abelian.epi_pullback_of_epi_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization, FormalCoproduct.homPullbackEquiv_symm_apply_φ, CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve, Types.range_pullbackFst, cospanExt_app_one, CategoryTheory.Over.monObjMkPullbackSnd_mul, diagonalObjPullbackFstIso_inv_fst_fst, TopCat.snd_isOpenEmbedding_of_left, PullbackCone.π_app_right, PushoutCocone.unop_π_app, CategoryTheory.Over.grpObjMkPullbackSnd_one, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left', CategoryTheory.Over.grpObjMkPullbackSnd_mul, FormalCoproduct.pullbackCone_fst_φ, PullbackCone.condition, Types.pullbackIsoPullback_hom_fst, CategoryTheory.IsPullback.isLimit', pullbackDiagonalMapIso.inv_fst_assoc, pullback_diagonal_map_snd_snd_fst_assoc, diagonalObjPullbackFstIso_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, CompHausLike.pullback.isLimit_lift, PullbackCone.unop_inl, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, TopCat.pullback_topology, PullbackCone.mk_π_app, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, PullbackCone.IsLimit.lift_fst, prodIsoPullback_inv_fst_assoc, PullbackCone.op_pt, equalizerPullbackMapIso_inv_ι_snd, pullbackConeOfLeftIso_π_app_right, diagonalObjPullbackFstIso_inv_snd_fst, pullbackObjIso_inv_comp_fst_assoc, PullbackCone.IsLimit.equivPullbackObj_apply_fst, equalizerPullbackMapIso_inv_ι_fst, pullbackConeOfLeftIso_snd, diagonalObjPullbackFstIso_hom_fst_fst_assoc, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, PullbackCone.condition_assoc, CategoryTheory.Over.preservesTerminalIso_pullback, PullbackCone.unop_inr, spanOp_hom_app, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left, TopCat.fst_iso_of_right_embedding_range_subset, PullbackCone.combine_π_app, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, equalizerPullbackMapIso_hom_fst_assoc, pullback.comp_diagonal_assoc, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, pullbackConeEquivBinaryFan_functor_map_hom, PullbackCone.op_inr, prodIsoPullback_hom_fst_assoc, AlgebraicGeometry.IsOpenImmersion.instπWalkingCospanSchemeCospanOne, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right, PullbackCone.op_ι_app, pullbackConeEquivBinaryFan_counitIso, pullback_diagonal_map_snd_fst_fst, diagramIsoCospan_hom_app, diagonalObjPullbackFstIso_inv_snd_snd, IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, cospan_left, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map, cospanExt_app_right, TopCat.range_pullback_map, CategoryTheory.Subobject.pullback_obj, pullback_lift_diagonal_isPullback, PullbackCone.mono_fst_of_is_pullback_of_mono, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, cospan_map_inr, cospanCompIso_inv_app_left, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, Cone.ofPullbackCone_pt, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackToBaseIsOpenImmersion, spanOp_inv_app, cospan_map_inl, CategoryTheory.Over.tensorHom_left_snd_assoc, PullbackCone.isIso_fst_of_mono_of_isLimit, Types.pullbackLimitCone_cone, Cone.ofPullbackCone_π, pullbackConeOfRightIso_π_app_right, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right, PullbackCone.snd_limit_cone, PullbackCone.mk_π_app_right, opSpan_hom_app, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', pullbackConeOfRightIso_fst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right, pullbackConeOfRightIso_x, PullbackCone.mk_π_app_one, TopCat.Sheaf.interUnionPullbackConeLift_right, preservesPullback_symmetry, hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair, CategoryTheory.IsPullback.of_isLimit, TopCat.fst_isEmbedding_of_right, isPullback_map_snd_snd, pullbackConeEquivBinaryFan_inverse_obj, pullbackConeEquivBinaryFan_functor_obj, CategoryTheory.Abelian.epi_snd_of_isLimit, TopCat.isOpenEmbedding_of_pullback, opCospan_hom_app, PullbackCone.IsLimit.equivPullbackObj_apply_snd, Types.pullbackIsoPullback_inv_snd, PullbackCone.π_app_left, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Square.isPullback_iff, TopCat.pullbackIsoProdSubtype_inv_snd_apply, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_left, TopCat.pullbackIsoProdSubtype_inv_fst, cospanCompIso_inv_app_right, FormalCoproduct.homPullbackEquiv_symm_apply_f_coe, PullbackCone.eta_inv_hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst, diagonalObjPullbackFstIso_inv_snd_fst_assoc, PushoutCocone.op_π_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl, opCospan_inv_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left, TopCat.pullbackIsoProdSubtype_hom_snd, cospanExt_inv_app_one, PullbackCone.unop_ι_app, Types.pullbackIsoPullback_hom_snd, CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone, pullbackDiagonalMapIso.hom_snd, pullbackConeOfLeftIso_π_app_none, CategoryTheory.Over.μ_pullback_left_fst_fst', TopCat.snd_iso_of_left_embedding_range_subset, pullbackObjIso_hom_comp_fst, cospanOp_hom_app, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.monObjMkPullbackSnd_one, TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, PullbackCone.isoMk_inv_hom, pullback_diagonal_map_snd_fst_fst_assoc, PreservesPullback.of_iso_comparison, pullbackDiagonalMapIso.inv_snd_fst, prodIsoPullback_hom_snd, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right, CategoryTheory.Regular.instHasCoequalizerFstSnd, cospan_right, cospanExt_app_left, TopCat.range_pullback_to_prod, TopCat.Sheaf.interUnionPullbackConeLift_left, PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, TopCat.pullback_fst_image_snd_preimage, CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, CompleteLattice.pullback_eq_inf, CategoryTheory.Abelian.epi_pullback_of_epi_g, prodIsoPullback_hom_snd_assoc, pullbackConeOfRightIso_π_app_left, pullbackConeOfLeftIso_x, CompHausLike.pullback.cone_π, TopCat.pullbackIsoProdSubtype_inv_fst_apply, pullbackObjIso_hom_comp_fst_assoc, CategoryTheory.Over.tensorHom_left_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeSndIsOpenImmersion, pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, equalizerPullbackMapIso_hom_snd_assoc, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso, pullback.comp_diagonal, cospanExt_hom_app_one, cospan_map_id, CategoryTheory.Over.tensorHom_left_fst_assoc, prodIsoPullback_hom_fst, PullbackCone.eta_hom_hom, CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr', AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, CategoryTheory.Over.η_pullback_left, PullbackCone.mk_pt, cospanCompIso_inv_app_one, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left, PullbackCone.ofCone_π, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1, pullbackObjIso_inv_comp_fst, PullbackCone.op_inl, PullbackCone.IsLimit.lift_snd, equalizerPullbackMapIso_hom_snd, diagonalObjPullbackFstIso_hom_fst_snd, PullbackCone.flip_pt, Types.pullbackIsoPullback_inv_fst, Types.pullbackIsoPullback_inv_fst_apply, cospanCompIso_hom_app_left, equalizerPullbackMapIso_hom_fst, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.MonoOver.pullback_obj_left, TopCat.pullbackIsoProdSubtype_hom_apply, CoproductDisjoint.nonempty_isInitial_of_ne, pullbackDiagonalMapIso.inv_snd_fst_assoc, equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, FormalCoproduct.pullbackCone_fst_f, pullback.diagonal_comp, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', pullbackObjIso_hom_comp_snd_assoc, CategoryTheory.MorphismProperty.diagonal_iff, Types.range_pullbackSnd, CompHausLike.instHasLimitWalkingCospanCospan, TopCat.fst_isOpenEmbedding_of_right, cospanCompIso_hom_app_one, pullback_diagonal_map_snd_snd_fst, prodIsoPullback_inv_snd, PullbackCone.combine_pt_map, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, CategoryTheory.NormalMonoCategory.pullback_of_mono, PullbackCone.unop_pt, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, diagonalObjPullbackFstIso_inv_fst_fst_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight, PullbackCone.combine_pt_obj, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_left, PushoutCocone.op_pt, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_left, FormalCoproduct.pullbackCone_condition, CategoryTheory.regularTopology.equalizerCondition_w, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion, pullbackConeOfRightIso_π_app_none, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.Over.μ_pullback_left_snd, Types.pullbackLimitCone_isLimit, CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right, diagonalObjPullbackFstIso_hom_fst_snd_assoc, cospanExt_inv_app_left, PullbackCone.condition_one, CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit, pullbackObjIso_inv_comp_snd_assoc, pullbackDiagonalMapIso.inv_snd_snd_assoc, TopCat.pullback_map_isEmbedding, diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, cospanOp_inv_app, cospanCompIso_hom_app_right, diagonalObjPullbackFstIso_hom_fst_fst, pullbackDiagonalMapIso.hom_fst_assoc, PullbackCone.isIso_snd_of_mono_of_isLimit, cospanCompIso_app_one, CategoryTheory.Abelian.epi_fst_of_isLimit, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong, CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike, CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1, PullbackCone.IsLimit.lift_fst_assoc, cospanCompIso_app_left, CategoryTheory.Over.tensorHom_left_snd, PushoutCocone.unop_pt, CategoryTheory.Presieve.uncurry_pullbackArrows, prodIsoPullback_inv_snd_assoc, CategoryTheory.Over.lift_left, PullbackCone.IsLimit.lift_snd_assoc, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget, PullbackCone.isoMk_hom_hom, pullback_map_eq_pullbackFstFstIso_inv, CategoryTheory.mono_iff_isIso_fst, AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective, PullbackCone.ofCone_pt, PullbackCone.mk_π_app_left, diagonalObjPullbackFstIso_inv_fst_snd, FormalCoproduct.homPullbackEquiv_apply_coe, pullbackConeEquivBinaryFan_unitIso, CategoryTheory.Over.isMonHom_pullbackFst_id_right, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.Over.tensorObj_left, CategoryTheory.mono_iff_isIso_snd, equalizerPullbackMapIso_inv_ι_fst_assoc, Types.pullbackIsoPullback_inv_snd_apply, PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd, PullbackCone.mono_snd_of_is_pullback_of_mono, TopCat.pullback_snd_range, opSpan_inv_app, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', TopCat.snd_isEmbedding_of_left, pullbackObjIso_inv_comp_snd, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, cospanExt_inv_app_right, CategoryTheory.Over.ε_pullback_left, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_reflectsPullback_of_right, pullback_fst_map_snd_isPullback, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective, CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, cospanExt_hom_app_right, AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left', pullbackDiagonalMapIso.inv_snd_snd, pullbackFstFstIso_inv, SSet.instFinitePullback, TopCat.pullback_fst_range, cospanExt_hom_app_left, FormalCoproduct.pullbackCone_snd_f, cospan_one, diagonal_pullback_fst, AlgebraicGeometry.LocallyRingedSpace.GlueData.instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, TopCat.pullback_snd_image_fst_preimage, pullback_lift_map_isPullback, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instSndPullbackConeOfLeft, FormalCoproduct.pullbackCone_snd_φ, CategoryTheory.Over.tensorObj_hom, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, FormalCoproduct.isPullback, cospanCompIso_app_right, pullbackConeEquivBinaryFan_inverse_map_hom, CompHausLike.pullback.cone_pt, PullbackCone.fst_limit_cone, pullbackObjIso_hom_comp_snd, TopCat.isEmbedding_of_pullback, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, pullback_equalizer, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullbackOfLeft, CategoryTheory.Regular.instMonoDesc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right
|
cospanCompIso 📖 | CompOp | 9 mathmath: cospanCompIso_inv_app_left, cospanCompIso_inv_app_right, cospanCompIso_inv_app_one, cospanCompIso_hom_app_left, cospanCompIso_hom_app_one, cospanCompIso_hom_app_right, cospanCompIso_app_one, cospanCompIso_app_left, cospanCompIso_app_right
|
cospanExt 📖 | CompOp | 9 mathmath: cospanExt_app_one, cospanExt_app_right, cospanExt_inv_app_one, cospanExt_app_left, cospanExt_hom_app_one, cospanExt_inv_app_left, cospanExt_inv_app_right, cospanExt_hom_app_right, cospanExt_hom_app_left
|
cospanHomMk 📖 | CompOp | 3 mathmath: PullbackCone.combine_π_app, PullbackCone.combine_pt_map, cospanHomMk_app
|
cospanIsoMk 📖 | CompOp | 2 mathmath: cospanIsoMk_inv_app, cospanIsoMk_hom_app
|
diagramIsoCospan 📖 | CompOp | 6 mathmath: diagramIsoCospan_inv_app, diagramIsoCospan_hom_app, Cone.ofPullbackCone_π, PullbackCone.isoMk_inv_hom, PullbackCone.ofCone_π, PullbackCone.isoMk_hom_hom
|
diagramIsoSpan 📖 | CompOp | 6 mathmath: PushoutCocone.isoMk_inv_hom, PushoutCocone.ofCocone_ι, Cocone.ofPushoutCocone_ι, PushoutCocone.isoMk_hom_hom, diagramIsoSpan_inv_app, diagramIsoSpan_hom_app
|
span 📖 | CompOp | 161 mathmath: spanCompIso_app_left, pushoutCoconeOfLeftIso_ι_app_right, PushoutCocone.flip_pt, CommRingCat.pushoutCocone_pt, spanCompIso_inv_app_zero, PushoutCocone.mk_ι_app_zero, PushoutCocone.inl_colimit_cocone, inl_coprodIsoPushout_hom, PushoutCocone.unop_π_app, inl_comp_pushoutObjIso_hom, pushoutCoconeEquivBinaryCofan_inverse_obj, pushoutCoconeEquivBinaryCofan_functor_obj, pushoutCoconeEquivBinaryCofan_unitIso, AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, PushoutCocone.condition_assoc, span_map_id, PushoutCocone.op_snd, PushoutCocone.isoMk_inv_hom, PullbackCone.op_pt, span_right, inr_comp_pushoutObjIso_hom_assoc, PushoutCocone.epi_inl_of_is_pushout_of_epi, CategoryTheory.IsPushout.isColimit', pushoutCoconeEquivBinaryCofan_inverse_map_hom, CommRingCat.Under.preservesFiniteLimits_of_flat, hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, spanCompIso_hom_app_zero, PushoutCocone.condition, spanOp_hom_app, CategoryTheory.Under.postAdjunctionRight_unit_app_right, spanExt_hom_app_right, spanCompIso_inv_app_left, Types.instMonoPushoutInl, PullbackCone.op_ι_app, span_map_snd, spanCompIso_app_zero, PushoutCocone.ofCocone_ι, spanExt_hom_app_zero, CommRingCat.HomTopology.isEmbedding_pushout, spanOp_inv_app, PushoutCocone.eta_inv_hom, inr_coprodIsoPushout_hom_assoc, opSpan_hom_app, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, spanCompIso_app_right, pushoutCoconeOfRightIso_x, CommRingCat.Under.instPreservesFiniteProductsUnderPushout, PushoutCocone.condition_zero, PushoutCocone.ι_app_left, pushoutCoconeOfLeftIso_ι_app_left, PushoutCocone.ofCocone_pt, spanExt_app_one, opCospan_hom_app, PushoutCocone.isIso_inl_of_epi_of_isColimit, CategoryTheory.SmallObject.ιFunctorObj_eq, CommRingCat.inr_injective_of_flat, spanCompIso_inv_app_right, PushoutCocone.mk_ι_app, PushoutCocone.ι_app_right, CategoryTheory.Abelian.mono_pushout_of_mono_g, spanExt_inv_app_zero, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, spanExt_app_left, CategoryTheory.BicartesianSq.isColimit', pushoutCoconeEquivBinaryCofan_functor_map_hom, PushoutCocone.IsColimit.inl_desc_assoc, PushoutCocone.inr_colimit_cocone, PushoutCocone.op_π_app, CompleteLattice.pushout_eq_sup, opCospan_inv_app, PullbackCone.unop_ι_app, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, cospanOp_hom_app, AlgebraicGeometry.instMonoObjWalkingSpanCompSchemeSpanForgetNoneWalkingPairSomeMapInitOfIsOpenImmersion, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, pushoutCoconeOfRightIso_ι_app_left, spanCompIso_hom_app_right, AlgebraicGeometry.isPullback_Spec_map_pushout, Types.pushoutCocone_inr_mono_of_isColimit, AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan, PushoutCocone.mk_pt, PushoutCocone.IsColimit.inr_desc_assoc, CommRingCat.inl_injective_of_flat, pushoutCoconeOfLeftIso_ι_app_none, PushoutCocone.IsColimit.inr_desc, spanCompIso_hom_app_left, CategoryTheory.SmallObject.πFunctorObj_eq, inl_comp_pushoutObjIso_inv, PushoutCocone.epi_inr_of_is_pushout_of_epi, inr_comp_pushoutObjIso_inv, spanExt_hom_app_left, CommRingCat.tensorProdIsoPushout_app, CategoryTheory.Square.isPushout_iff, Cocone.ofPushoutCocone_ι, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, inl_comp_pushoutObjIso_inv_assoc, IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right, CategoryTheory.MorphismProperty.ind_underObj_pushout, inr_coprodIsoPushout_hom, PushoutCocone.IsColimit.inl_desc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Abelian.mono_inl_of_isColimit, PullbackCone.unop_pt, span_map_fst, pushoutCoconeOfLeftIso_x, PushoutCocone.op_pt, PushoutCocone.mk_ι_app_right, span_left, inl_comp_pushoutObjIso_hom_assoc, AlgebraicGeometry.isPullback_SpecMap_pushout, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, inl_coprodIsoPushout_inv, AlgebraicGeometry.isIso_pushoutSection_iff, PreservesPushout.of_iso_comparison, PushoutCocone.isoMk_hom_hom, cospanOp_inv_app, pushoutCoconeOfRightIso_ι_app_none, PushoutCocone.mk_ι_app_left, CategoryTheory.Abelian.mono_pushout_of_mono_f, Types.Pushout.cocone_ι_app, CategoryTheory.epi_iff_isIso_inl, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, inr_coprodIsoPushout_inv, PushoutCocone.unop_pt, PushoutCocone.eta_hom_hom, spanExt_app_right, inl_coprodIsoPushout_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, pushoutCoconeEquivBinaryCofan_counitIso, inr_comp_pushoutObjIso_inv_assoc, Types.instMonoPushoutInr, inr_comp_pushoutObjIso_hom, CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization, CategoryTheory.Abelian.mono_inr_of_isColimit, diagramIsoSpan_inv_app, AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit, CategoryTheory.IsPushout.of_isColimit, span_zero, preservesPushout_symmetry, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, Cocone.ofPushoutCocone_pt, inl_coprodIsoPushout_inv_assoc, opSpan_inv_app, PushoutCocone.isIso_inr_of_epi_of_isColimit, pushoutCoconeOfRightIso_ι_app_right, CategoryTheory.NormalEpiCategory.pushout_of_epi, inr_coprodIsoPushout_inv_assoc, PushoutCocone.unop_snd, CategoryTheory.epi_iff_isIso_inr, diagramIsoSpan_hom_app, PushoutCocone.unop_fst, PushoutCocone.op_fst, Types.pushoutCocone_inr_injective_of_isColimit, spanExt_inv_app_right, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, RingHom.IsStableUnderBaseChange.pushout_inl, spanExt_inv_app_left, Types.Pushout.cocone_pt, CategoryTheory.IsPushout.isVanKampen_iff, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
|
spanCompIso 📖 | CompOp | 9 mathmath: spanCompIso_app_left, spanCompIso_inv_app_zero, spanCompIso_hom_app_zero, spanCompIso_inv_app_left, spanCompIso_app_zero, spanCompIso_app_right, spanCompIso_inv_app_right, spanCompIso_hom_app_right, spanCompIso_hom_app_left
|
spanExt 📖 | CompOp | 9 mathmath: spanExt_hom_app_right, spanExt_hom_app_zero, spanExt_app_one, spanExt_inv_app_zero, spanExt_app_left, spanExt_hom_app_left, spanExt_app_right, spanExt_inv_app_right, spanExt_inv_app_left
|
spanHomMk 📖 | CompOp | 1 mathmath: spanHomMk_app
|
spanIsoMk 📖 | CompOp | 2 mathmath: spanIsoMk_hom_app, spanIsoMk_inv_app
|