HasPullback

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

Statistics

Metric	Count
Definitions HasPullback, HasPullbacks, HasPullbacksAlong, HasPushout, HasPushouts, HasPushoutsAlong, pullback, cone, congrHom, desc', fst, isLimit, lift', map, mapDesc, snd, pullbackComparison, pullbackIsPullback, pullbackProdFstIsoProd, pullbackProdSndIsoProd, pullbackSymmetry, pushout, cocone, congrHom, desc, inl, inr, isColimit, map, mapLift, pushoutComparison, pushoutIsPushout, pushoutSymmetry, walkingCospanOpEquiv, walkingSpanOpEquiv	35
Theorems fst_limit_cone, snd_limit_cone, inl_colimit_cocone, inr_colimit_cocone, hasPullback_symmetry, hasPullback_symmetry_of_hasPullbacksAlong, hasPullbacks_of_hasLimit_cospan, hasPullbacks_of_hasWidePullbacks, hasPushout_symmetry, hasPushouts_of_hasColimit_span, hasPushouts_of_hasWidePushouts, hasPushouts_symmetry_of_hasPushoutsAlong, inl_comp_pushoutComparison, inl_comp_pushoutComparison_assoc, inl_comp_pushoutSymmetry_hom, inl_comp_pushoutSymmetry_hom_assoc, inl_comp_pushoutSymmetry_inv, inl_comp_pushoutSymmetry_inv_assoc, inr_comp_pushoutComparison, inr_comp_pushoutComparison_assoc, inr_comp_pushoutSymmetry_hom, inr_comp_pushoutSymmetry_hom_assoc, inr_comp_pushoutSymmetry_inv, inr_comp_pushoutSymmetry_inv_assoc, map_lift_pullbackComparison, map_lift_pullbackComparison_assoc, condition, condition_assoc, congrHom_hom, congrHom_inv, exists_lift, hom_ext, hom_ext_iff, lift_fst, lift_fst_assoc, lift_fst_snd, lift_snd, lift_snd_assoc, mapDesc_comp, map_comp, map_comp_assoc, map_id, map_isIso, pullbackComparison_comp_fst, pullbackComparison_comp_fst_assoc, pullbackComparison_comp_snd, pullbackComparison_comp_snd_assoc, pullbackProdFstIsoProd_hom_fst, pullbackProdFstIsoProd_hom_fst_assoc, pullbackProdFstIsoProd_hom_snd, pullbackProdFstIsoProd_hom_snd_assoc, pullbackProdFstIsoProd_inv_fst, pullbackProdFstIsoProd_inv_fst_assoc, pullbackProdFstIsoProd_inv_snd_fst, pullbackProdFstIsoProd_inv_snd_fst_assoc, pullbackProdFstIsoProd_inv_snd_snd, pullbackProdFstIsoProd_inv_snd_snd_assoc, pullbackProdSndIsoProd_hom_fst, pullbackProdSndIsoProd_hom_fst_assoc, pullbackProdSndIsoProd_hom_snd, pullbackProdSndIsoProd_hom_snd_assoc, pullbackProdSndIsoProd_inv_fst_fst, pullbackProdSndIsoProd_inv_fst_fst_assoc, pullbackProdSndIsoProd_inv_fst_snd, pullbackProdSndIsoProd_inv_fst_snd_assoc, pullbackProdSndIsoProd_inv_snd, pullbackProdSndIsoProd_inv_snd_assoc, pullbackSymmetry_hom_comp_fst, pullbackSymmetry_hom_comp_fst_assoc, pullbackSymmetry_hom_comp_snd, pullbackSymmetry_hom_comp_snd_assoc, pullbackSymmetry_inv_comp_fst, pullbackSymmetry_inv_comp_fst_assoc, pullbackSymmetry_inv_comp_snd, pullbackSymmetry_inv_comp_snd_assoc, condition, condition_assoc, congrHom_hom, congrHom_inv, desc_inl_inr, exists_desc, hom_ext, hom_ext_iff, inl_desc, inl_desc_assoc, inr_desc, inr_desc_assoc, mapLift_comp, map_comp, map_comp_assoc, map_id, map_isIso, pushoutComparison_map_desc, pushoutComparison_map_desc_assoc, walkingCospanOpEquiv_counitIso_hom_app, walkingCospanOpEquiv_counitIso_inv_app, walkingCospanOpEquiv_functor_map, walkingCospanOpEquiv_functor_obj, walkingCospanOpEquiv_inverse_map, walkingCospanOpEquiv_inverse_obj, walkingCospanOpEquiv_unitIso_hom_app, walkingCospanOpEquiv_unitIso_inv_app, walkingSpanOpEquiv_counitIso_hom_app, walkingSpanOpEquiv_counitIso_inv_app, walkingSpanOpEquiv_functor_map, walkingSpanOpEquiv_functor_obj, walkingSpanOpEquiv_inverse_map, walkingSpanOpEquiv_inverse_obj, walkingSpanOpEquiv_unitIso_hom_app, walkingSpanOpEquiv_unitIso_inv_app	110
Total	145

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasPullback 📖	MathDef	55 math math: hasPullbackVertPaste, CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows, hasPullback_symmetry, hasPullback_of_left_iso, CategoryTheory.HasPullbacksOfInclusions.preservesPullbackInl', has_kernel_pair_of_mono, CategoryTheory.GlueData.instHasPullbackMapF, FormalCoproduct.instHasPullback, CategoryTheory.IsPullback.instHasPullbackFst, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_right, FormalCoproduct.hasPullback_of_pullbackCone, CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr, AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback, CategoryTheory.Adhesive.hasPullback_of_mono_left, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀, CategoryTheory.HasPullbacksOfInclusions.hasPullbackInl, CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong, CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct, CategoryTheory.MorphismProperty.hasPullback, hasPullback_of_right_factors_mono, AlgebraicGeometry.Scheme.Pullback.affine_affine_hasPullback, hasPullback_assoc, hasPullback_symmetry_of_hasPullbacksAlong, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right, hasPullback_assoc_symm, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left, HasPullback.of_createsLimit, CategoryTheory.IsPullback.hasPullback, AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right, CategoryTheory.instHasPullbackF', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_left, CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_inclusions, CategoryTheory.Presieve.HasPullbacks.hasPullback, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left, hasPullback_of_preservesPullback, AlgebraicGeometry.Scheme.Pullback.base_affine_hasPullback, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1, hasPullback_of_left_factors_mono, CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks, CategoryTheory.Presieve.hasPullback, AlgebraicGeometry.Scheme.Pullback.instHasPullback, CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback, hasPullback_of_comp_mono, CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left, hasPullback_over_zero, hasPullback_of_right_iso, CategoryTheory.MorphismProperty.HasPullbacks.hasPullback, CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd, CategoryTheory.GlueData'.f_hasPullback, CategoryTheory.GlueData.f_hasPullback, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_right, hasPullbackHorizPaste, AlgebraicGeometry.Scheme.Pullback.affine_hasPullback, CategoryTheory.HasPullbacksOfInclusions.hasPullbackInr'
HasPullbacks 📖	MathDef	14 math math: CategoryTheory.MorphismProperty.Over.hasPullbacks, AlgebraicGeometry.Scheme.Pullback.instHasPullbacks, hasPullbacks_of_hasBinaryProducts_of_hasEqualizers, CategoryTheory.PreGaloisCategory.hasPullbacks, FormalCoproduct.instHasPullbacks, Types.instHasPullbacksType, CompHausLike.instHasPullbacksOfHasExplicitPullbacks, hasPullbacks_of_hasWidePullbacks, hasPullbacks_opposite, CategoryTheory.Over.instHasPullbacks, CategoryTheory.ChosenPullbacksAlong.hasPullbacks, CategoryTheory.Abelian.hasPullbacks, hasPullbacks_of_hasLimit_cospan, AlgebraicGeometry.Scheme.instHasPullbacksEtale
HasPullbacksAlong 📖	MathDef	1 math math: CategoryTheory.ChosenPullbacksAlong.hasPullbackAlong
HasPushout 📖	MathDef	18 math math: hasPushout_assoc, hasPushout_of_right_factors_epi, hasPushoutVertPaste, hasPushout_of_epi_comp, CategoryTheory.IsPushout.hasPushout, has_cokernel_pair_of_epi, hasPushout_assoc_symm, hasPushout_of_preservesPushout, CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd, instHasPushoutComp, CategoryTheory.Adhesive.hasPushout_of_mono_left, hasPushout_of_right_iso, hasPushout_symmetry, HasPushout.of_createsColimit, hasPushouts_symmetry_of_hasPushoutsAlong, hasPushout_of_left_iso, hasPushout_over_zero, hasPushout_of_left_factors_epi
HasPushouts 📖	MathDef	8 math math: Types.instHasPushoutsType, hasPushouts_opposite, CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts, CategoryTheory.Abelian.hasPushouts, hasPushouts_of_hasColimit_span, hasPushouts_of_hasWidePushouts, CategoryTheory.SmallObject.hasPushouts, hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers
HasPushoutsAlong 📖	MathDef	—
pullback 📖	CompOp	708 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁, CategoryTheory.Over.associator_hom_left_snd_fst_assoc, AlgebraicGeometry.Surjective.instFstScheme, pushoutIsoOpPullback_inr_hom_assoc, CategoryTheory.Over.prodLeftIsoPullback_hom_snd_assoc, HomotopicalAlgebra.instFibrationFstOfIsStableUnderBaseChangeFibrations, CategoryTheory.Over.μ_pullback_left_snd', AlgebraicGeometry.instLocallyQuasiFiniteSndScheme, TopCat.pullbackIsoProdSubtype_hom_fst, pullbackDiagonalMapIdIso_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, pullbackIsoUnopPushout_inv_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_X, CategoryTheory.PreZeroHypercover.pullback₁_X, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian, diagonalObjPullbackFstIso_inv_snd_snd_assoc, AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1, pullback.instIsSplitEpiFst, pullback_inv_snd_fst_of_left_isIso, CategoryTheory.IsPullback.isoPullback_inv_fst, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, pullbackProdSndIsoProd_hom_snd, CategoryTheory.Over.associator_inv_left_snd, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst, AlgebraicGeometry.Etale.instFstScheme, pullbackDiagonalMapIso.hom_fst, pushoutIsoOpPullback_inl_hom, diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.instLocallyQuasiFiniteFstScheme, CategoryTheory.Over.pullback_obj_left, CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, pullbackFstFstIso_hom, CategoryTheory.IsPullback.isoPullback_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, pullbackSymmetry_inv_comp_snd_assoc, prodIsoPullback_inv_fst, HomotopicalAlgebra.PrepathObject.trans_p₀, CategoryTheory.Abelian.epi_pullback_of_epi_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.MorphismProperty.pullback_snd_iff, pullbackDiagonalMapIdIso_inv_snd_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.IsProper.instFstScheme, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, Types.range_pullbackFst, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst, AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme, CategoryTheory.Over.monObjMkPullbackSnd_mul, diagonalObjPullbackFstIso_inv_fst_fst, TopCat.snd_isOpenEmbedding_of_left, AlgebraicGeometry.diagonal_SpecMap, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_snd_of_left, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃_assoc, Concrete.pullbackMk_snd, AlgebraicGeometry.IsProper.instSndScheme, pullbackDiagonalMapIdIso_inv_snd_snd_assoc, pullbackProdSndIsoProd_inv_fst_snd, CategoryTheory.Over.grpObjMkPullbackSnd_one, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, pullbackAssoc_hom_snd_fst_assoc, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_I₀, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, pullbackIsoOpPushout_hom_inr_assoc, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, pushoutIsoUnopPullback_inr_hom, Types.pullbackIsoPullback_hom_fst, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, pullback_snd_iso_of_left_iso, pullbackDiagonalMapIso.inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle, AlgebraicGeometry.Scheme.Cover.gluedCover_t, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, pullbackRightPullbackFstIso_hom_fst, pullbackLeftPullbackSndIso_inv_fst_snd_assoc, pushoutIsoUnopPullback_inl_hom_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, pullbackProdFstIsoProd_hom_fst_assoc, pullbackAssoc_inv_fst_snd, CategoryTheory.Over.braiding_inv_left, pullback.lift_fst_assoc, CategoryTheory.Over.prodLeftIsoPullback_inv_snd, pushoutIsoUnopPullback_inr_hom_assoc, PreservesPullback.iso_inv_fst_assoc, AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo, AlgebraicGeometry.instGeometricallyReducedSndScheme, CategoryTheory.GlueData.t'_iij, pullback_diagonal_map_snd_snd_fst_assoc, diagonalObjPullbackFstIso_hom_snd, pullbackIsoUnopPushout_hom_inr_assoc, CategoryTheory.IsPullback.instHasPullbackFst, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, TopCat.pullback_topology, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, CategoryTheory.MorphismProperty.Over.pullback_obj_left, prodIsoPullback_inv_fst_assoc, AlgebraicGeometry.IsIntegralHom.instSndScheme, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, pushoutIsoUnopPullback_inv_snd, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd, equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.PreZeroHypercover.pullback₂_X, pullbackAssoc_inv_fst_snd_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assoc, diagonalObjPullbackFstIso_inv_snd_fst, pullbackObjIso_inv_comp_fst_assoc, HomotopicalAlgebra.PrepathObject.trans_P, equalizerPullbackMapIso_inv_ι_fst, pushoutIsoUnopPullback_inv_fst, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, pullbackLeftPullbackSndIso_inv_fst, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, diagonalObjPullbackFstIso_hom_fst_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, CategoryTheory.Over.whiskerRight_left_fst, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, AlgebraicGeometry.instGeometricallyIntegralSndScheme, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, pullback.lift_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, CategoryTheory.Over.prodLeftIsoPullback_inv_fst, pullbackIsoUnopPushout_hom_inl, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, pullbackProdSndIsoProd_hom_fst, AlgebraicGeometry.Scheme.Pullback.cocycle, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, TopCat.fst_iso_of_right_embedding_range_subset, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, CategoryTheory.Over.prodLeftIsoPullback_inv_snd_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, CategoryTheory.Over.mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd_assoc, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, equalizerPullbackMapIso_hom_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion, AlgebraicGeometry.Flat.instFstScheme, pullback.comp_diagonal_assoc, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.pullbackSpecIso_inv_snd, AlgebraicGeometry.IsImmersion.instMapDescScheme, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, AlgebraicGeometry.Etale.instSndScheme, AlgebraicGeometry.Scheme.Cover.gluedCover_V, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, prodIsoPullback_hom_fst_assoc, CategoryTheory.Over.prodLeftIsoPullback_hom_snd, PreservesPullback.iso_inv_snd, HomotopicalAlgebra.PrepathObject.trans_p₁, PreservesPullback.iso_inv_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, pullback_diagonal_map_snd_fst_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft, diagonalObjPullbackFstIso_inv_snd_snd, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.pullbackSpecIso_hom_base, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, CategoryTheory.Over.associator_inv_left_fst_fst_assoc, AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback, pullbackSymmetry_inv_comp_fst_assoc, CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, CategoryTheory.Over.associator_hom_left_fst, CategoryTheory.MorphismProperty.baseChange_map', AlgebraicGeometry.Scheme.isMonHom_fst_id_right, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, pullbackZeroZeroIso_inv_fst, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, CategoryTheory.IsPullback.isoPullback_inv_snd, pullbackZeroZeroIso_hom_snd, CategoryTheory.Over.prodLeftIsoPullback_hom_fst_assoc, pullbackIsoOpPushout_inv_fst_assoc, TopCat.range_pullback_map, CategoryTheory.GlueData.t'_iji, CategoryTheory.Subobject.pullback_obj, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, pullback_lift_diagonal_isPullback, AlgebraicGeometry.instGeometricallyReducedFstScheme, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', AlgebraicGeometry.Scheme.Pullback.t_snd, pullbackRightPullbackFstIso_hom_snd, pullback.lift_snd_assoc, pullbackProdFstIsoProd_inv_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, CategoryTheory.ShortComplex.SnakeInput.snd_δ, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, pullback.map_id, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.instIsClosedImmersionSndScheme, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_X, AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', pullback.instIsSplitEpiSnd, pullbackIsoUnopPushout_inv_fst, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, PreservesPullback.iso_hom_fst, pullbackLeftPullbackSndIso_inv_fst_snd, AlgebraicGeometry.instGeometricallyIrreducibleSndScheme, pullback.exists_lift, pullbackProdSndIsoProd_inv_fst_snd_assoc, CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_f, pullbackProdFstIsoProd_inv_snd_snd, pullback.diagonal_isKernelPair, pushoutIsoOpPullback_inv_fst, pullbackAssoc_hom_snd_snd, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, CategoryTheory.GlueData.t_fac, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, AlgebraicGeometry.UniversallyOpen.snd, TopCat.fst_isEmbedding_of_right, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, pullbackRightPullbackFstIso_hom_fst_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth, isPullback_map_snd_snd, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd_assoc, CategoryTheory.Over.associator_hom_left_snd_fst, CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_I₀, AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType_1, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, PreservesPullback.iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, CategoryTheory.PreZeroHypercover.inter_f, pullbackDiagonalMapIdIso_inv_fst, CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry_assoc, CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, Types.pullbackIsoPullback_inv_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, AlgebraicGeometry.instQuasiCompactSndScheme, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, AlgebraicGeometry.IsFinite.instFstScheme, TopCat.pullbackIsoProdSubtype_inv_snd_apply, pushoutIsoUnopPullback_inl_hom, hasPullback_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left, pullbackAssoc_hom_snd_fst, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, pullbackProdFstIsoProd_inv_snd_fst, HomotopicalAlgebra.PathObject.trans_p₀, CategoryTheory.Over.pullback_map_left, pullback.condition_assoc, pullbackDiagonalMapIdIso_inv_fst_assoc, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, pullbackRightPullbackFstIso_inv_fst, TopCat.pullbackIsoProdSubtype_inv_fst, pullbackIsoOpPushout_inv_fst, AlgebraicGeometry.Scheme.Pullback.gluing_U, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, CategoryTheory.GlueData.t_fac_assoc, pullbackIsoOpPushout_inv_snd, pullbackLeftPullbackSndIso_hom_snd_assoc, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc, CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_I₀, diagonalObjPullbackFstIso_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι, AlgebraicGeometry.UniversallyOpen.fst, CategoryTheory.Over.associator_inv_left_fst_snd, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, pullback.map_comp_assoc, AlgebraicGeometry.IsIntegralHom.instFstScheme, AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme, pullbackProdFstIsoProd_inv_snd_snd_assoc, hasPullback_assoc_symm, pullbackProdSndIsoProd_inv_fst_fst, CategoryTheory.Over.associator_hom_left_snd_snd_assoc, TopCat.pullbackIsoProdSubtype_hom_snd, AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1, pullback_map_diagonal_isPullback, pullback.map_comp, Types.pullbackIsoPullback_hom_snd, pullbackDiagonalMapIso.hom_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, CategoryTheory.Over.μ_pullback_left_fst_fst', TopCat.snd_iso_of_left_embedding_range_subset, pullbackObjIso_hom_comp_fst, pullbackRightPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Presieve.ofArrows_pullback, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.monObjMkPullbackSnd_one, isIso_fst_of_mono, TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂_assoc, AlgebraicGeometry.instQuasiSeparatedSndScheme, pullbackSymmetry_hom_of_mono_eq, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, pullbackRightPullbackFstIso_inv_fst_assoc, AlgebraicGeometry.IsFinite.instSndScheme, pullback_snd_iso_of_left_factors_mono, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, pullback_diagonal_map_snd_fst_fst_assoc, AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme, CategoryTheory.GlueData.t'_inv, pullbackProdSndIsoProd_inv_fst_fst_assoc, AlgebraicGeometry.instGeometricallyIntegralFstScheme, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, CategoryTheory.IsPullback.isoPullback_hom_fst, pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_f, pullbackProdFstIsoProd_inv_fst_assoc, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, CategoryTheory.GlueData.t'_jii, prodIsoPullback_hom_snd, CategoryTheory.Regular.instHasCoequalizerFstSnd, HomotopicalAlgebra.instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, PreservesPullback.iso_hom_snd_assoc, TopCat.range_pullback_to_prod, CategoryTheory.Presieve.pullback_singleton, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, CategoryTheory.GlueData.cocycle_assoc, TopCat.pullback_fst_image_snd_preimage, CompleteLattice.pullback_eq_inf, CategoryTheory.Abelian.epi_pullback_of_epi_g, AlgebraicGeometry.Surjective.instSndScheme, pullbackDiagonalMapIdIso_hom_fst_assoc, prodIsoPullback_hom_snd_assoc, CategoryTheory.Over.associator_inv_left_fst_fst, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, AlgebraicGeometry.universallyClosed_fst, pushoutIsoOpPullback_inr_hom, TopCat.pullbackIsoProdSubtype_inv_fst_apply, AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType, CategoryTheory.GlueData'.cocycle_assoc, pullbackObjIso_hom_comp_fst_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', CategoryTheory.Over.tensorHom_left_fst, CategoryTheory.GlueData'.cocycle, CategoryTheory.PreZeroHypercover.inter_X, AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId, AlgebraicGeometry.IsImmersion.instFstScheme, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, pullbackComparison_comp_snd_assoc, pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst, pullback.fst_of_mono, pullbackAssoc_hom_snd_snd_assoc, CategoryTheory.regularTopology.equalizerCondition_w', AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo, equalizerPullbackMapIso_hom_snd_assoc, pullbackLeftPullbackSndIso_hom_snd, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, pullbackZeroZeroIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, pullback.comp_diagonal, pullbackIsoOpPushout_hom_inl, prodIsoPullback_hom_fst, instIsIsoPullbackComparison, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.instHasLiftingPropertyFst, pullback.snd_of_mono, CategoryTheory.Over.prodLeftIsoPullback_inv_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, pullbackProdFstIsoProd_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd, CategoryTheory.MorphismProperty.pullback_fst_iff, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.MorphismProperty.pullback_map, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, pullback.hom_ext_iff, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, AlgebraicGeometry.instQuasiCompactFstScheme, CategoryTheory.MonoOver.inf_map_app, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, pullbackObjIso_inv_comp_fst, pullbackAssoc_inv_snd_assoc, equalizerPullbackMapIso_hom_snd, pullback_inv_snd_fst_of_left_isIso_assoc, pullbackIsoUnopPushout_hom_inl_assoc, AlgebraicGeometry.pullbackSpecIso_hom_fst, diagonalObjPullbackFstIso_hom_fst_snd, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst_assoc, Types.pullbackIsoPullback_inv_fst, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, CategoryTheory.instHasLiftingPropertySnd, Types.pullbackIsoPullback_inv_fst_apply, equalizerPullbackMapIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, TopCat.isEmbedding_pullback_to_prod, CategoryTheory.MonoOver.pullback_obj_left, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme, TopCat.pullbackIsoProdSubtype_hom_apply, pullbackDiagonalMapIso.inv_snd_fst_assoc, equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, CategoryTheory.instIsRegularEpiSnd, pullbackSymmetry_inv_comp_fst, pullback.diagonal_comp, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme, pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullbackIsoUnopPushout_inv_fst_assoc, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, pullbackObjIso_hom_comp_snd_assoc, pushoutIsoOpPullback_inl_hom_assoc, Types.range_pullbackSnd, pullback_snd_iso_of_right_factors_mono, AlgebraicGeometry.IsPreimmersion.instSndScheme, TopCat.fst_isOpenEmbedding_of_right, pullback_diagonal_map_snd_snd_fst, prodIsoPullback_inv_snd, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, AlgebraicGeometry.Scheme.Pullback.range_fst, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.instIsClosedImmersionFstScheme, pullback_inv_fst_snd_of_right_isIso, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, diagonalObjPullbackFstIso_inv_fst_fst_assoc, pullbackDiagonalMapIdIso_inv_snd_snd, pullbackSymmetry_hom_comp_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁_assoc, pullbackSymmetry_hom_comp_snd, CategoryTheory.PreOneHypercover.inter_Y, CategoryTheory.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.IsPullback.isoPullback_hom_snd_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀, CategoryTheory.IsKernelPair.pullback, CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀, CategoryTheory.MorphismProperty.Over.pullback_map_left, pullbackProdSndIsoProd_hom_snd_assoc, pullbackComparison_comp_fst, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂, AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo, pullbackComparison_comp_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.Over.μ_pullback_left_snd, pullbackLeftPullbackSndIso_hom_fst_assoc, CategoryTheory.MorphismProperty.pullback_snd, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, AlgebraicGeometry.pullbackSpecIso_hom_base_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, pullbackZeroZeroIso_inv_snd, diagonalObjPullbackFstIso_hom_fst_snd_assoc, pullbackLeftPullbackSndIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, CategoryTheory.GlueData'.t_fac, pullbackIsoOpPushout_hom_inr, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, pullbackObjIso_inv_comp_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, pullbackDiagonalMapIso.inv_snd_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst_assoc, CategoryTheory.Over.braiding_hom_left, TopCat.pullback_map_isEmbedding, diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_I₀, HomotopicalAlgebra.instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, AlgebraicGeometry.geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, pullbackAssoc_hom_fst, PreservesPullback.iso_hom_fst_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, pullback_inv_fst_snd_of_right_isIso_assoc, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, AlgebraicGeometry.pullbackSpecIso_inv_fst', pullbackDiagonalMapIdIso_hom_snd_assoc, CategoryTheory.PreOneHypercover.toPullback_cylinder, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, pullbackSymmetry_hom_comp_fst_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, diagonalObjPullbackFstIso_hom_fst_fst, pullbackDiagonalMapIso.hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, pushoutIsoOpPullback_inv_snd, AlgebraicGeometry.IsPreimmersion.instFstScheme, AlgebraicGeometry.pullback_of_geometrically', AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.canonicallyOverPullback_over, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, pullbackIsoOpPushout_inv_snd_assoc, pullbackLeftPullbackSndIso_inv_snd_snd, CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, AlgebraicGeometry.diagonal_Spec_map, AlgebraicGeometry.instQuasiSeparatedFstScheme, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne, CategoryTheory.Over.tensorHom_left_snd, pullback.mapDesc_comp, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, pullbackProdFstIsoProd_hom_snd_assoc, AlgebraicGeometry.Flat.instSndScheme, CategoryTheory.IsPullback.isoPullback_inv_fst_assoc, CategoryTheory.Presieve.uncurry_pullbackArrows, pullbackSymmetry_inv_comp_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian, prodIsoPullback_inv_snd_assoc, AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_pt, pullback.condition, pullbackProdSndIsoProd_inv_snd_assoc, CategoryTheory.IsPullback.isoPullback_hom_snd, CategoryTheory.IsKernelPair.of_hasPullback, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.instGeometricallyIrreducibleFstScheme, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_fst_of_right, CategoryTheory.GlueData.cocycle, pullbackProdFstIsoProd_hom_fst, AlgebraicGeometry.instSmoothSndScheme, mono_pullback_to_prod, pullbackProdSndIsoProd_inv_snd, CategoryTheory.GlueData.t'_isIso, AlgebraicGeometry.pullbackSpecIso_hom_fst', AlgebraicGeometry.IsImmersion.instSndScheme, pullbackDiagonalMapIdIso_hom_snd, pullbackIsoOpPushout_hom_inl_assoc, pullback_map_eq_pullbackFstFstIso_inv, pullback.congrHom_inv, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.PreOneHypercover.cylinder_p₁, HomotopicalAlgebra.instFibrationSndOfIsStableUnderBaseChangeFibrations, PreservesPullback.iso_hom_snd, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, Concrete.pullbackMk_fst, pullback_fst_iso_of_right_iso, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, map_lift_pullbackComparison, isIso_snd_of_mono, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, pullback.congrHom_hom, AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective, pullbackIsoUnopPushout_inv_snd_assoc, pullback.lift_fst, pullbackRightPullbackFstIso_inv_snd_fst, pullbackLeftPullbackSndIso_inv_snd_snd_assoc, CategoryTheory.Over.prodLeftIsoPullback_hom_fst, diagonalObjPullbackFstIso_inv_fst_snd, CategoryTheory.Over.associator_hom_left_fst_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_SpecTensorTo, map_lift_pullbackComparison_assoc, CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext_iff, PreservesPullback.iso_hom, CategoryTheory.Over.isMonHom_pullbackFst_id_right, pullbackComparison_comp_fst_assoc, AlgebraicGeometry.pullbackSpecIso_hom_snd, AlgebraicGeometry.instSmoothFstScheme, CategoryTheory.instIsRegularEpiFst, AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, AlgebraicGeometry.Scheme.isEmpty_pullback, pullbackSymmetry_hom_comp_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, CategoryTheory.Over.tensorObj_left, CategoryTheory.PreZeroHypercover.toPreOneHypercover_Y, equalizerPullbackMapIso_inv_ι_fst_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, Types.pullbackIsoPullback_inv_snd_apply, pullbackAssoc_inv_snd, TopCat.pullback_snd_range, pullbackIsoUnopPushout_hom_inr, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁_assoc, TopCat.snd_isEmbedding_of_left, pullbackObjIso_inv_comp_snd, pullbackAssoc_inv_fst_fst_assoc, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, CategoryTheory.Over.ε_pullback_left, pullback.lift_fst_snd, pullback_fst_map_snd_isPullback, CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry, pullback.map_isIso, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_fst_of_right, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, pullbackRightPullbackFstIso_hom_snd_assoc, AlgebraicGeometry.IsSeparated.instFstScheme, pullbackAssoc_hom_fst_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X, pullbackDiagonalMapIdIso_hom_fst, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, pullbackLeftPullbackSndIso_inv_fst_assoc, CategoryTheory.IsPullback.isoPullback_hom_fst_assoc, pullbackProdFstIsoProd_hom_snd, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, CategoryTheory.GlueData.mapGlueData_t', CategoryTheory.Over.associator_hom_left_snd_snd, CategoryTheory.Over.associator_inv_left_snd_assoc, AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom, pullbackDiagonalMapIso.inv_snd_snd, AlgebraicGeometry.IsSeparated.instSndScheme, AlgebraicGeometry.IsOpenImmersion.instSndScheme, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, pullbackFstFstIso_inv, SSet.instFinitePullback, TopCat.pullback_fst_range, AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc, AlgebraicGeometry.IsOpenImmersion.instFstScheme, CategoryTheory.Over.whiskerLeft_left_snd, HomotopicalAlgebra.PathObject.trans_p₁, diagonal_pullback_fst, TopCat.pullback_snd_image_fst_preimage, pullback_lift_map_isPullback, HomotopicalAlgebra.PathObject.trans_P, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X, CategoryTheory.PreOneHypercover.cylinderHom_h₀, AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, CategoryTheory.Over.tensorObj_hom, pullbackRightPullbackFstIso_inv_snd_snd, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine, pullbackAssoc_inv_fst_fst, CategoryTheory.PreOneHypercover.cylinder_Y, AlgebraicGeometry.pullback_of_geometrically, pullbackObjIso_hom_comp_snd, AlgebraicGeometry.universallyClosed_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, CategoryTheory.Regular.instMonoDesc, pullbackProdSndIsoProd_hom_fst_assoc, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc
pullbackComparison 📖	CompOp	10 math math: pullbackComparison_comp_snd_assoc, instIsIsoPullbackComparison, pullbackComparison_comp_fst, pullbackComparison_comp_snd, map_lift_pullbackComparison, AlgebraicGeometry.Scheme.Pullback.forget_comparison_surjective, map_lift_pullbackComparison_assoc, PreservesPullback.iso_hom, pullbackComparison_comp_fst_assoc, AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective
pullbackIsPullback 📖	CompOp	—
pullbackProdFstIsoProd 📖	CompOp	12 math math: pullbackProdFstIsoProd_hom_fst_assoc, pullbackProdFstIsoProd_inv_fst, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, pullbackProdFstIsoProd_inv_snd_snd, pullbackProdFstIsoProd_inv_snd_fst, pullbackProdFstIsoProd_inv_snd_snd_assoc, pullbackProdFstIsoProd_inv_fst_assoc, pullbackProdFstIsoProd_inv_snd_fst_assoc, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, pullbackProdFstIsoProd_hom_snd_assoc, pullbackProdFstIsoProd_hom_fst, pullbackProdFstIsoProd_hom_snd
pullbackProdSndIsoProd 📖	CompOp	10 math math: pullbackProdSndIsoProd_hom_snd, pullbackProdSndIsoProd_inv_fst_snd, pullbackProdSndIsoProd_hom_fst, pullbackProdSndIsoProd_inv_fst_snd_assoc, pullbackProdSndIsoProd_inv_fst_fst, pullbackProdSndIsoProd_inv_fst_fst_assoc, pullbackProdSndIsoProd_hom_snd_assoc, pullbackProdSndIsoProd_inv_snd_assoc, pullbackProdSndIsoProd_inv_snd, pullbackProdSndIsoProd_hom_fst_assoc
pullbackSymmetry 📖	CompOp	24 math math: pullbackSymmetry_inv_comp_snd_assoc, AlgebraicGeometry.Scheme.Cover.gluedCover_t, CategoryTheory.Over.braiding_inv_left, CategoryTheory.GlueData.t'_iij, pullbackSymmetry_inv_comp_fst_assoc, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry_assoc, CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀, pullbackSymmetry_hom_of_mono_eq, CategoryTheory.GlueData.t'_inv, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, pullbackSymmetry_inv_comp_fst, pullbackSymmetry_hom_comp_snd_assoc, pullbackSymmetry_hom_comp_snd, CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀, CategoryTheory.Over.braiding_hom_left, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, pullbackSymmetry_hom_comp_fst_assoc, pullbackSymmetry_inv_comp_snd, pullbackSymmetry_hom_comp_fst, CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry, diagonal_pullback_fst, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
pushout 📖	CompOp	193 math math: pushoutIsoOpPullback_inr_hom_assoc, CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.instHasLiftingPropertyInl, hasPushout_assoc, PreservesPushout.inr_iso_inv_assoc, pullbackIsoUnopPushout_inv_snd, pushoutIsoOpPullback_inl_hom, pushout.inr_desc, PreservesPushout.inr_iso_inv, inl_coprodIsoPushout_hom, inr_inl_pushoutRightPushoutInlIso_hom_assoc, inl_comp_pushoutComparison_assoc, pullbackIsoOpPushout_hom_inr_assoc, pushout_inr_iso_of_left_iso, inl_inr_pushoutAssoc_inv_assoc, inl_comp_pushoutObjIso_hom, pushoutIsoUnopPullback_inr_hom, PreservesPushout.inr_iso_hom_assoc, instIsIsoPushoutComparison, inr_inr_pushoutRightPushoutInlIso_hom, pushoutIsoUnopPullback_inl_hom_assoc, pushoutIsoUnopPullback_inr_hom_assoc, inl_pushoutAssoc_inv_assoc, inr_inl_pushoutLeftPushoutInrIso_hom, pullbackIsoUnopPushout_hom_inr_assoc, inr_comp_pushoutObjIso_hom_assoc, pushoutIsoUnopPullback_inv_snd, pushout.condition, inr_inl_pushoutRightPushoutInlIso_hom, inl_comp_pushoutComparison, CategoryTheory.Under.pushout_map, CategoryTheory.IsPushout.inr_isoPushout_inv_assoc, pushoutIsoUnopPullback_inv_fst, inr_pushoutLeftPushoutInrIso_inv, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.IsPushout.inr_isoPushout_hom_assoc, inl_inl_pushoutLeftPushoutInrIso_hom_assoc, pullbackIsoUnopPushout_hom_inl, CategoryTheory.IsPushout.inr_isoPushout_inv, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_pt, Types.instMonoPushoutInl, pullback_symmetry_hom_of_epi_eq, inr_pushoutZeroZeroIso_hom, inr_pushoutLeftPushoutInrIso_inv_assoc, hasPushout_assoc_symm, inl_inl_pushoutLeftPushoutInrIso_hom, pushout.inl_desc_assoc, PreservesPushout.inl_iso_inv, pullbackIsoOpPushout_inv_fst_assoc, inr_pushoutAssoc_hom_assoc, CategoryTheory.Under.mapPushoutAdj_unit_app, inl_pushoutRightPushoutInlIso_inv, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, pushout.hom_ext_iff, CommRingCat.HomTopology.isEmbedding_pushout, inr_coprodIsoPushout_hom_assoc, HomotopicalAlgebra.instCofibrationInrOfIsStableUnderCobaseChangeCofibrations, pushoutComparison_map_desc, pushout_inr_inv_inl_of_right_isIso_assoc, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, PreservesPushout.inl_iso_inv_assoc, HomotopicalAlgebra.instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, pullbackIsoUnopPushout_inv_fst, pushoutIsoOpPullback_inv_fst, pushout.inl_of_epi, CommRingCat.inr_injective_of_flat, CategoryTheory.Abelian.mono_pushout_of_mono_g, pushout_inr_iso_of_right_factors_epi, inr_comp_pushoutSymmetry_inv_assoc, pushoutIsoUnopPullback_inl_hom, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.MorphismProperty.pushout_inr, pullbackIsoOpPushout_inv_fst, inr_pushoutAssoc_hom, pullbackIsoOpPushout_inv_snd, pushout.exists_desc, inl_comp_pushoutSymmetry_inv, HomotopicalAlgebra.Precylinder.trans_I, inl_pushoutLeftPushoutInrIso_inv, CompleteLattice.pushout_eq_sup, inr_comp_pushoutSymmetry_hom_assoc, PreservesPushout.inl_iso_hom_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, inr_pushoutRightPushoutInlIso_inv, epi_coprod_to_pushout, PreservesPushout.inr_iso_hom, pushout_inl_iso_of_left_factors_epi, CategoryTheory.MorphismProperty.pushout_inl, HomotopicalAlgebra.Cylinder.trans_i₀, CategoryTheory.IsPushout.inl_isoPushout_inv, inl_inl_pushoutAssoc_hom, HomotopicalAlgebra.instCofibrationInlOfIsStableUnderCobaseChangeCofibrations, AlgebraicGeometry.isPullback_Spec_map_pushout, inr_inr_pushoutRightPushoutInlIso_hom_assoc, pushoutIsoOpPullback_inr_hom, pushout.map_comp, inl_inr_pushoutAssoc_inv, pushout.map_comp_assoc, pullbackIsoOpPushout_hom_inl, pushout.desc_inl_inr, CommRingCat.inl_injective_of_flat, CategoryTheory.instHasLiftingPropertyInr, inl_comp_pushoutObjIso_inv, pullbackIsoUnopPushout_hom_inl_assoc, inr_comp_pushoutObjIso_inv, pushoutComparison_map_desc_assoc, inr_comp_pushoutSymmetry_inv, CategoryTheory.Under.pushout_obj, CategoryTheory.IsPushout.inl_isoPushout_hom, inr_pushoutZeroZeroIso_inv, HomotopicalAlgebra.instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, inl_pushoutLeftPushoutInrIso_inv_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, inr_pushoutRightPushoutInlIso_inv_assoc, inl_comp_pushoutObjIso_inv_assoc, pullbackIsoUnopPushout_inv_fst_assoc, pushoutIsoOpPullback_inl_hom_assoc, HomotopicalAlgebra.Cylinder.trans_I, CategoryTheory.IsPushout.inl_isoPushout_hom_assoc, inr_coprodIsoPushout_hom, inr_inl_pushoutAssoc_hom, pushout_inl_iso_of_right_iso, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.MorphismProperty.pushout_inr_iff, inl_comp_pushoutSymmetry_inv_assoc, pushout.congrHom_hom, CategoryTheory.IsPushout.inl_isoPushout_inv_assoc, inr_comp_pushoutComparison_assoc, pushout.mapLift_comp, inl_comp_pushoutObjIso_hom_assoc, CategoryTheory.Under.mapPushoutAdj_counit_app, HomotopicalAlgebra.Cylinder.trans_i₁, AlgebraicGeometry.isPullback_SpecMap_pushout, inl_pushoutAssoc_inv, inl_inl_pushoutAssoc_hom_assoc, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, pullbackIsoOpPushout_hom_inr, inl_pushoutRightPushoutInlIso_hom, inr_inr_pushoutAssoc_inv_assoc, inl_coprodIsoPushout_inv, AlgebraicGeometry.isIso_pushoutSection_iff, inl_pushoutZeroZeroIso_inv, inl_pushoutRightPushoutInlIso_hom_assoc, pushout_inl_inv_inr_of_right_isIso_assoc, pushout.inr_desc_assoc, inl_comp_pushoutSymmetry_hom_assoc, pushoutIsoOpPullback_inv_snd, PreservesPushout.inl_iso_hom, CategoryTheory.Abelian.mono_pushout_of_mono_f, pullbackIsoOpPushout_inv_snd_assoc, inl_comp_pushoutSymmetry_hom, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, isIso_inr_of_epi, inr_coprodIsoPushout_inv, pushout.inl_desc, inr_inl_pushoutLeftPushoutInrIso_hom_assoc, inl_coprodIsoPushout_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, inr_comp_pushoutObjIso_inv_assoc, Types.instMonoPushoutInr, inr_comp_pushoutObjIso_hom, inr_pushoutLeftPushoutInrIso_hom_assoc, pullbackIsoOpPushout_hom_inl_assoc, pushout_inl_inv_inr_of_right_isIso, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, CategoryTheory.IsPushout.inr_isoPushout_hom, pushout.congrHom_inv, pullbackIsoUnopPushout_inv_snd_assoc, inl_coprodIsoPushout_inv_assoc, inr_inl_pushoutAssoc_hom_assoc, pullbackIsoUnopPushout_hom_inr, inr_pushoutLeftPushoutInrIso_hom, HomotopicalAlgebra.Precylinder.trans_i₁, inr_coprodIsoPushout_inv_assoc, pushout.condition_assoc, pushout_inr_inv_inl_of_right_isIso, inl_pushoutRightPushoutInlIso_inv_assoc, HomotopicalAlgebra.Precylinder.trans_i₀, pushout.map_id, pushout.map_isIso, inl_pushoutZeroZeroIso_hom, isIso_inl_of_epi, inr_inr_pushoutAssoc_inv, inr_comp_pushoutSymmetry_hom, CategoryTheory.MorphismProperty.pushout_inl_iff, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, RingHom.IsStableUnderBaseChange.pushout_inl, PreservesPushout.iso_hom, inr_comp_pushoutComparison, pushout.inr_of_epi, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
pushoutComparison 📖	CompOp	8 math math: inl_comp_pushoutComparison_assoc, instIsIsoPushoutComparison, inl_comp_pushoutComparison, pushoutComparison_map_desc, pushoutComparison_map_desc_assoc, inr_comp_pushoutComparison_assoc, PreservesPushout.iso_hom, inr_comp_pushoutComparison
pushoutIsPushout 📖	CompOp	—
pushoutSymmetry 📖	CompOp	9 math math: pullback_symmetry_hom_of_epi_eq, inr_comp_pushoutSymmetry_inv_assoc, inl_comp_pushoutSymmetry_inv, inr_comp_pushoutSymmetry_hom_assoc, inr_comp_pushoutSymmetry_inv, inl_comp_pushoutSymmetry_inv_assoc, inl_comp_pushoutSymmetry_hom_assoc, inl_comp_pushoutSymmetry_hom, inr_comp_pushoutSymmetry_hom
walkingCospanOpEquiv 📖	CompOp	14 math math: PushoutCocone.unop_π_app, walkingCospanOpEquiv_counitIso_hom_app, spanOp_hom_app, walkingCospanOpEquiv_counitIso_inv_app, PullbackCone.op_ι_app, walkingCospanOpEquiv_inverse_obj, walkingCospanOpEquiv_unitIso_inv_app, spanOp_inv_app, opCospan_hom_app, opCospan_inv_app, walkingCospanOpEquiv_functor_map, walkingCospanOpEquiv_functor_obj, walkingCospanOpEquiv_unitIso_hom_app, walkingCospanOpEquiv_inverse_map
walkingSpanOpEquiv 📖	CompOp	14 math math: walkingSpanOpEquiv_inverse_map, walkingSpanOpEquiv_inverse_obj, opSpan_hom_app, walkingSpanOpEquiv_counitIso_hom_app, PushoutCocone.op_π_app, walkingSpanOpEquiv_unitIso_inv_app, PullbackCone.unop_ι_app, cospanOp_hom_app, walkingSpanOpEquiv_functor_map, cospanOp_inv_app, walkingSpanOpEquiv_functor_obj, walkingSpanOpEquiv_unitIso_hom_app, walkingSpanOpEquiv_counitIso_inv_app, opSpan_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullback_symmetry 📖	mathematical	—	HasPullback	—	pullback.condition
hasPullback_symmetry_of_hasPullbacksAlong 📖	mathematical	HasPullbacksAlong	HasPullback	—	hasPullback_symmetry
hasPullbacks_of_hasLimit_cospan 📖	mathematical	HasLimit WalkingCospan WidePullbackShape.category WalkingPair cospan	HasPullbacks	—	hasLimit_of_iso
hasPullbacks_of_hasWidePullbacks 📖	mathematical	HasWidePullbacks	HasPullbacks	—	hasWidePullbacks_shrink
hasPushout_symmetry 📖	mathematical	—	HasPushout	—	pushout.condition
hasPushouts_of_hasColimit_span 📖	mathematical	HasColimit WalkingSpan WidePushoutShape.category WalkingPair span	HasPushouts	—	hasColimit_of_iso
hasPushouts_of_hasWidePushouts 📖	mathematical	HasWidePushouts	HasPushouts	—	hasWidePushouts_shrink
hasPushouts_symmetry_of_hasPushoutsAlong 📖	mathematical	HasPushoutsAlong	HasPushout	—	hasPushout_symmetry
inl_comp_pushoutComparison 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pushout CategoryTheory.Functor.map pushout.inl pushoutComparison	—	pushout.inl_desc
inl_comp_pushoutComparison_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pushout CategoryTheory.Functor.map pushout.inl pushoutComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_comp_pushoutComparison
inl_comp_pushoutSymmetry_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inl CategoryTheory.Iso.hom pushoutSymmetry pushout.inr	—	IsColimit.comp_coconePointUniqueUpToIso_hom hasPushout_symmetry pushout.condition
inl_comp_pushoutSymmetry_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inl hasPushout_symmetry CategoryTheory.Iso.hom pushoutSymmetry pushout.inr	—	hasPushout_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_comp_pushoutSymmetry_hom
inl_comp_pushoutSymmetry_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inl CategoryTheory.Iso.inv pushoutSymmetry pushout.inr	—	hasPushout_symmetry inr_comp_pushoutSymmetry_hom
inl_comp_pushoutSymmetry_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inl CategoryTheory.Iso.inv pushoutSymmetry pushout.inr	—	hasPushout_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_comp_pushoutSymmetry_inv
inr_comp_pushoutComparison 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pushout CategoryTheory.Functor.map pushout.inr pushoutComparison	—	pushout.inr_desc
inr_comp_pushoutComparison_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pushout CategoryTheory.Functor.map pushout.inr pushoutComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_pushoutComparison
inr_comp_pushoutSymmetry_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inr CategoryTheory.Iso.hom pushoutSymmetry pushout.inl	—	IsColimit.comp_coconePointUniqueUpToIso_hom hasPushout_symmetry pushout.condition
inr_comp_pushoutSymmetry_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout pushout.inr hasPushout_symmetry CategoryTheory.Iso.hom pushoutSymmetry pushout.inl	—	hasPushout_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_pushoutSymmetry_hom
inr_comp_pushoutSymmetry_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inr CategoryTheory.Iso.inv pushoutSymmetry pushout.inl	—	hasPushout_symmetry inl_comp_pushoutSymmetry_hom
inr_comp_pushoutSymmetry_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pushout hasPushout_symmetry pushout.inr CategoryTheory.Iso.inv pushoutSymmetry pushout.inl	—	hasPushout_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_pushoutSymmetry_inv
map_lift_pullbackComparison 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullback.lift pullbackComparison	—	pullback.hom_ext CategoryTheory.Category.assoc pullbackComparison_comp_fst CategoryTheory.Functor.map_comp limit.lift_π pullbackComparison_comp_snd
map_lift_pullbackComparison_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullback.lift pullbackComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_lift_pullbackComparison
pullbackComparison_comp_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullbackComparison pullback.fst	—	pullback.lift_fst
pullbackComparison_comp_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullbackComparison pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackComparison_comp_fst
pullbackComparison_comp_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullbackComparison pullback.snd	—	pullback.lift_snd
pullbackComparison_comp_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj pullback CategoryTheory.Functor.map pullbackComparison pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackComparison_comp_snd
pullbackProdFstIsoProd_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.fst CategoryTheory.Iso.hom pullbackProdFstIsoProd pullback.fst	—	limit.lift_π
pullbackProdFstIsoProd_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.fst CategoryTheory.Iso.hom pullbackProdFstIsoProd pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdFstIsoProd_hom_fst
pullbackProdFstIsoProd_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.fst CategoryTheory.Iso.hom pullbackProdFstIsoProd prod.snd pullback.snd	—	limit.lift_π
pullbackProdFstIsoProd_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.fst CategoryTheory.Iso.hom pullbackProdFstIsoProd prod.snd pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdFstIsoProd_hom_snd
pullbackProdFstIsoProd_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.fst	—	limit.lift_π
pullbackProdFstIsoProd_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdFstIsoProd_inv_fst
pullbackProdFstIsoProd_inv_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.snd	—	limit.lift_π_assoc prod.map_fst
pullbackProdFstIsoProd_inv_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdFstIsoProd_inv_snd_fst
pullbackProdFstIsoProd_inv_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.snd prod.snd	—	limit.lift_π_assoc prod.map_snd CategoryTheory.Category.comp_id
pullbackProdFstIsoProd_inv_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.fst CategoryTheory.Iso.inv pullbackProdFstIsoProd pullback.snd prod.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdFstIsoProd_inv_snd_snd
pullbackProdSndIsoProd_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.snd CategoryTheory.Iso.hom pullbackProdSndIsoProd prod.fst pullback.fst	—	limit.lift_π
pullbackProdSndIsoProd_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.snd CategoryTheory.Iso.hom pullbackProdSndIsoProd prod.fst pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdSndIsoProd_hom_fst
pullbackProdSndIsoProd_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.snd CategoryTheory.Iso.hom pullbackProdSndIsoProd pullback.snd	—	limit.lift_π
pullbackProdSndIsoProd_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback prod prod.snd CategoryTheory.Iso.hom pullbackProdSndIsoProd pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdSndIsoProd_hom_snd
pullbackProdSndIsoProd_inv_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.fst prod.fst	—	limit.lift_π_assoc prod.map_fst CategoryTheory.Category.comp_id
pullbackProdSndIsoProd_inv_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.fst prod.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdSndIsoProd_inv_fst_fst
pullbackProdSndIsoProd_inv_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.fst	—	limit.lift_π_assoc prod.map_snd
pullbackProdSndIsoProd_inv_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdSndIsoProd_inv_fst_snd
pullbackProdSndIsoProd_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.snd	—	limit.lift_π
pullbackProdSndIsoProd_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct prod pullback prod.snd CategoryTheory.Iso.inv pullbackProdSndIsoProd pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackProdSndIsoProd_inv_snd
pullbackSymmetry_hom_comp_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.hom pullbackSymmetry pullback.fst pullback.snd	—	hasPullback_symmetry limit.conePointUniqueUpToIso_hom_comp pullback.condition
pullbackSymmetry_hom_comp_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.hom pullbackSymmetry pullback.fst pullback.snd	—	hasPullback_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSymmetry_hom_comp_fst
pullbackSymmetry_hom_comp_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.hom pullbackSymmetry pullback.snd pullback.fst	—	hasPullback_symmetry limit.conePointUniqueUpToIso_hom_comp pullback.condition
pullbackSymmetry_hom_comp_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.hom pullbackSymmetry pullback.snd pullback.fst	—	hasPullback_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSymmetry_hom_comp_snd
pullbackSymmetry_inv_comp_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.inv pullbackSymmetry pullback.fst pullback.snd	—	hasPullback_symmetry pullbackSymmetry_hom_comp_snd
pullbackSymmetry_inv_comp_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.inv pullbackSymmetry pullback.fst pullback.snd	—	hasPullback_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSymmetry_inv_comp_fst
pullbackSymmetry_inv_comp_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.inv pullbackSymmetry pullback.snd pullback.fst	—	hasPullback_symmetry pullbackSymmetry_hom_comp_fst
pullbackSymmetry_inv_comp_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback hasPullback_symmetry CategoryTheory.Iso.inv pullbackSymmetry pullback.snd pullback.fst	—	hasPullback_symmetry CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSymmetry_inv_comp_snd
pushoutComparison_map_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pushout CategoryTheory.Functor.obj CategoryTheory.Functor.map pushoutComparison pushout.desc	—	pushout.hom_ext inl_comp_pushoutComparison_assoc CategoryTheory.Functor.map_comp colimit.ι_desc inr_comp_pushoutComparison_assoc
pushoutComparison_map_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	pushout CategoryTheory.Functor.obj CategoryTheory.Functor.map pushoutComparison pushout.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushoutComparison_map_desc
walkingCospanOpEquiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WidePushoutShape WalkingPair WidePushoutShape.category CategoryTheory.Functor.comp Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category widePushoutShapeOp widePullbackShapeUnop CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso WalkingCospan WalkingSpan walkingCospanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingCospanOpEquiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WidePushoutShape WalkingPair WidePushoutShape.category CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category widePushoutShapeOp widePullbackShapeUnop CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso WalkingCospan WalkingSpan walkingCospanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingCospanOpEquiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite WidePullbackShape WalkingPair CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape WidePushoutShape.category CategoryTheory.Equivalence.functor WalkingCospan WalkingSpan walkingCospanOpEquiv Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct widePullbackShapeOpMap Opposite.unop	—	—
walkingCospanOpEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite WidePullbackShape WalkingPair CategoryTheory.Category.opposite WidePullbackShape.category WidePushoutShape WidePushoutShape.category CategoryTheory.Equivalence.functor WalkingCospan WalkingSpan walkingCospanOpEquiv Opposite.unop	—	—
walkingCospanOpEquiv_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map WidePushoutShape WalkingPair WidePushoutShape.category Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Equivalence.inverse WalkingCospan WalkingSpan walkingCospanOpEquiv widePushoutShapeOpMap	—	—
walkingCospanOpEquiv_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj WidePushoutShape WalkingPair WidePushoutShape.category Opposite WidePullbackShape CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Equivalence.inverse WalkingCospan WalkingSpan walkingCospanOpEquiv Opposite.op	—	—
walkingCospanOpEquiv_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WidePullbackShape WalkingPair CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Functor.id CategoryTheory.Functor.comp WidePushoutShape WidePushoutShape.category widePullbackShapeUnop widePushoutShapeOp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso WalkingCospan WalkingSpan walkingCospanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingCospanOpEquiv_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WidePullbackShape WalkingPair CategoryTheory.Category.opposite WidePullbackShape.category CategoryTheory.Functor.comp WidePushoutShape WidePushoutShape.category widePullbackShapeUnop widePushoutShapeOp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso WalkingCospan WalkingSpan walkingCospanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingSpanOpEquiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app WidePullbackShape WalkingPair WidePullbackShape.category CategoryTheory.Functor.comp Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category widePullbackShapeOp widePushoutShapeUnop CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso WalkingSpan WalkingCospan walkingSpanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingSpanOpEquiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app WidePullbackShape WalkingPair WidePullbackShape.category CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category widePullbackShapeOp widePushoutShapeUnop CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso WalkingSpan WalkingCospan walkingSpanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingSpanOpEquiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite WidePushoutShape WalkingPair CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape WidePullbackShape.category CategoryTheory.Equivalence.functor WalkingSpan WalkingCospan walkingSpanOpEquiv Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct widePushoutShapeOpMap Opposite.unop	—	—
walkingSpanOpEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite WidePushoutShape WalkingPair CategoryTheory.Category.opposite WidePushoutShape.category WidePullbackShape WidePullbackShape.category CategoryTheory.Equivalence.functor WalkingSpan WalkingCospan walkingSpanOpEquiv Opposite.unop	—	—
walkingSpanOpEquiv_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map WidePullbackShape WalkingPair WidePullbackShape.category Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Equivalence.inverse WalkingSpan WalkingCospan walkingSpanOpEquiv widePullbackShapeOpMap	—	—
walkingSpanOpEquiv_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj WidePullbackShape WalkingPair WidePullbackShape.category Opposite WidePushoutShape CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Equivalence.inverse WalkingSpan WalkingCospan walkingSpanOpEquiv Opposite.op	—	—
walkingSpanOpEquiv_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WidePushoutShape WalkingPair CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Functor.id CategoryTheory.Functor.comp WidePullbackShape WidePullbackShape.category widePushoutShapeUnop widePullbackShapeOp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso WalkingSpan WalkingCospan walkingSpanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
walkingSpanOpEquiv_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite WidePushoutShape WalkingPair CategoryTheory.Category.opposite WidePushoutShape.category CategoryTheory.Functor.comp WidePullbackShape WidePullbackShape.category widePushoutShapeUnop widePullbackShapeOp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso WalkingSpan WalkingCospan walkingSpanOpEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Limits.PullbackCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_limit_cone 📖	mathematical	—	fst CategoryTheory.Limits.limit.cone CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	—
snd_limit_cone 📖	mathematical	—	snd CategoryTheory.Limits.limit.cone CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	—

CategoryTheory.Limits.PushoutCocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl_colimit_cocone 📖	mathematical	—	inl CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inl	—	—
inr_colimit_cocone 📖	mathematical	—	inr CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inr	—	—

CategoryTheory.Limits.pullback

Definitions

Name	Category	Theorems
cone 📖	CompOp	—
congrHom 📖	CompOp	3 math math: mapDesc_comp, congrHom_inv, congrHom_hom
desc' 📖	CompOp	—
fst 📖	CompOp	434 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst, CategoryTheory.Over.associator_hom_left_snd_fst_assoc, AlgebraicGeometry.Surjective.instFstScheme, HomotopicalAlgebra.instFibrationFstOfIsStableUnderBaseChangeFibrations, CategoryTheory.Over.μ_pullback_left_snd', TopCat.pullbackIsoProdSubtype_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc, instIsSplitEpiFst, CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso, CategoryTheory.IsPullback.isoPullback_inv_fst, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, CategoryTheory.Over.associator_inv_left_snd, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst, AlgebraicGeometry.Etale.instFstScheme, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc, AlgebraicGeometry.instLocallyQuasiFiniteFstScheme, CategoryTheory.Limits.pullbackFstFstIso_hom, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_x, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc, prodIsoPullback_inv_fst, HomotopicalAlgebra.PrepathObject.trans_p₀, CategoryTheory.Over.rightUnitor_inv_left_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, AlgebraicGeometry.IsProper.instFstScheme, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, CategoryTheory.Limits.Types.range_pullbackFst, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd_assoc, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc, CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst_assoc, CategoryTheory.Limits.pullbackAssoc_inv_fst_snd, lift_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd, CategoryTheory.IsPullback.instHasPullbackFst, CategoryTheory.Over.tensorObj_ext_iff, TopCat.pullback_topology, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left, prodIsoPullback_inv_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_fst_assoc, CategoryTheory.Over.rightUnitor_inv_left_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst, CategoryTheory.Limits.pullbackObjIso_inv_comp_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst, CategoryTheory.Over.whiskerRight_left_fst, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, CategoryTheory.Over.prodLeftIsoPullback_inv_fst, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl, CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst, AlgebraicGeometry.Scheme.Pullback.cocycle, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, TopCat.fst_iso_of_right_embedding_range_subset, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, CategoryTheory.Over.mapPullbackAdj_counit_app, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, AlgebraicGeometry.Flat.instFstScheme, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, AlgebraicGeometry.Scheme.Pullback.range_fst_comp, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, prodIsoPullback_hom_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.pullbackSpecIso_hom_base, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, CategoryTheory.Over.associator_inv_left_fst_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc, CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, CategoryTheory.Over.associator_hom_left_fst, CategoryTheory.MorphismProperty.baseChange_map', AlgebraicGeometry.Scheme.isMonHom_fst_id_right, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst, CategoryTheory.Over.prodLeftIsoPullback_hom_fst_assoc, CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst_assoc, TopCat.range_pullback_map, CategoryTheory.GlueData.t'_iji, AlgebraicGeometry.instGeometricallyReducedFstScheme, AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst, CategoryTheory.Over.leftUnitor_inv_left_fst, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, CategoryTheory.MorphismProperty.pullback_fst, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', diagonal_fst, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, CategoryTheory.Limits.PreservesPullback.iso_hom_fst, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd, exists_lift, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_snd_assoc, diagonal_isKernelPair, CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, CategoryTheory.GlueData.t_fac, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, TopCat.fst_isEmbedding_of_right, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Limits.isPullback_map_snd_snd, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, CategoryTheory.Over.associator_hom_left_snd_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, CategoryTheory.PreZeroHypercover.inter_f, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, AlgebraicGeometry.pullbackSpecIso_inv_fst, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, AlgebraicGeometry.IsFinite.instFstScheme, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom, CategoryTheory.Limits.hasPullback_assoc, CategoryTheory.Limits.pullbackAssoc_hom_snd_fst, HomotopicalAlgebra.PathObject.trans_p₀, CategoryTheory.Over.pullback_map_left, condition_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst, TopCat.pullbackIsoProdSubtype_inv_fst, CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, CategoryTheory.GlueData.t_fac_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι, AlgebraicGeometry.UniversallyOpen.fst, CategoryTheory.Over.associator_inv_left_fst_snd, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.IsIntegralHom.instFstScheme, AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst, CategoryTheory.Over.associator_hom_left_snd_snd_assoc, CategoryTheory.Limits.pullback_map_diagonal_isPullback, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, CategoryTheory.Over.μ_pullback_left_fst_fst', CategoryTheory.Limits.pullbackObjIso_hom_comp_fst, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Limits.isIso_fst_of_mono, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc, CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst_assoc, AlgebraicGeometry.instGeometricallyIntegralFstScheme, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_fst, CategoryTheory.IsPullback.isoPullback_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst_assoc, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, CategoryTheory.GlueData.t'_jii, CategoryTheory.Regular.instHasCoequalizerFstSnd, HomotopicalAlgebra.instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, TopCat.range_pullback_to_prod, TopCat.pullback_fst_image_snd_preimage, CategoryTheory.Abelian.epi_pullback_of_epi_g, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc, CategoryTheory.Over.associator_inv_left_fst_fst, AlgebraicGeometry.universallyClosed_fst, TopCat.pullbackIsoProdSubtype_inv_fst_apply, CategoryTheory.Limits.pullbackObjIso_hom_comp_fst_assoc, CategoryTheory.Over.tensorHom_left_fst, AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId, AlgebraicGeometry.IsImmersion.instFstScheme, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst, fst_of_mono, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc, CategoryTheory.regularTopology.equalizerCondition_w', AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Cover.gluedCover_f, CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, CategoryTheory.Limits.fst_eq_snd_of_mono_eq, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl, CategoryTheory.Over.tensorHom_left_fst_assoc, prodIsoPullback_hom_fst, CategoryTheory.instHasLiftingPropertyFst, CategoryTheory.Over.prodLeftIsoPullback_inv_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, diagonal_fst_assoc, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right, CategoryTheory.MorphismProperty.pullback_fst_iff, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, hom_ext_iff, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, CategoryTheory.Over.whiskerLeft_left_fst, AlgebraicGeometry.instQuasiCompactFstScheme, CategoryTheory.MonoOver.inf_map_app, AlgebraicGeometry.Scheme.Pullback.Triplet.fst_SpecTensorTo_apply, CategoryTheory.Limits.pullbackObjIso_inv_comp_fst, CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd, CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc, AlgebraicGeometry.pullbackSpecIso_hom_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst_assoc, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, CategoryTheory.Over.whiskerLeft_left_fst_assoc, TopCat.isEmbedding_pullback_to_prod, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, TopCat.pullbackIsoProdSubtype_hom_apply, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc, CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom_assoc, TopCat.fst_isOpenEmbedding_of_right, CategoryTheory.Over.leftUnitor_inv_left_fst_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, AlgebraicGeometry.Scheme.Pullback.range_fst, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.instIsClosedImmersionFstScheme, CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd, CategoryTheory.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.IsKernelPair.pullback, CategoryTheory.Over.rightUnitor_hom_left, CategoryTheory.MorphismProperty.Over.pullback_map_left, CategoryTheory.Limits.pullbackComparison_comp_fst, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_fst'_eq_p₁, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst_assoc, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, AlgebraicGeometry.pullbackSpecIso_hom_base_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, CategoryTheory.GlueData'.t_fac, AlgebraicGeometry.AffineSpace.over_over, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc, AlgebraicGeometry.pullbackSpecIso_hom_fst'_assoc, CategoryTheory.Limits.pullbackAssoc_hom_fst, CategoryTheory.Limits.PreservesPullback.iso_hom_fst_assoc, CategoryTheory.Over.μ_pullback_left_fst_fst, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso_assoc, AlgebraicGeometry.pullbackSpecIso_inv_fst', CategoryTheory.PreOneHypercover.toPullback_cylinder, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, AlgebraicGeometry.IsPreimmersion.instFstScheme, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, AlgebraicGeometry.instQuasiSeparatedFstScheme, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, CategoryTheory.Over.whiskerRight_left_fst_assoc, CategoryTheory.PreZeroHypercover.interFst_h₀, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, CategoryTheory.IsPullback.isoPullback_inv_fst_assoc, CategoryTheory.PreZeroHypercover.pullback₁_f, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst_assoc, condition, CategoryTheory.IsKernelPair.of_hasPullback, AlgebraicGeometry.instGeometricallyIrreducibleFstScheme, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_fst_of_right, CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst, CategoryTheory.Limits.mono_pullback_to_prod, AlgebraicGeometry.pullbackSpecIso_hom_fst', CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl_assoc, CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv, CategoryTheory.PreOneHypercover.cylinder_p₁, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst, CategoryTheory.Limits.Concrete.pullbackMk_fst, CategoryTheory.Limits.pullback_fst_iso_of_right_iso, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback, lift_fst, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst, CategoryTheory.Over.fst_left, CategoryTheory.Over.prodLeftIsoPullback_hom_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd, CategoryTheory.Over.associator_hom_left_fst_assoc, CategoryTheory.Over.isMonHom_pullbackFst_id_right, CategoryTheory.Limits.pullbackComparison_comp_fst_assoc, AlgebraicGeometry.instSmoothFstScheme, CategoryTheory.instIsRegularEpiFst, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, CategoryTheory.Limits.pullbackAssoc_inv_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, lift_fst_snd, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_fst_of_right, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc, AlgebraicGeometry.IsSeparated.instFstScheme, CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_assoc, CategoryTheory.IsPullback.isoPullback_hom_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, CategoryTheory.Over.associator_hom_left_snd_snd, CategoryTheory.Over.associator_inv_left_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, CategoryTheory.Limits.pullbackFstFstIso_inv, TopCat.pullback_fst_range, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst, AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc, AlgebraicGeometry.IsOpenImmersion.instFstScheme, CategoryTheory.Limits.diagonal_pullback_fst, TopCat.pullback_snd_image_fst_preimage, CategoryTheory.Limits.pullback_lift_map_isPullback, CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc, CategoryTheory.PreOneHypercover.cylinderHom_h₀, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, CategoryTheory.Over.tensorObj_hom, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd, CategoryTheory.Limits.PullbackCone.fst_limit_cone, CategoryTheory.Limits.pullbackAssoc_inv_fst_fst, CategoryTheory.PreOneHypercover.cylinder_Y, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, CategoryTheory.Regular.instMonoDesc, CategoryTheory.Limits.pullbackProdSndIsoProd_hom_fst_assoc, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt
isLimit 📖	CompOp	—
lift' 📖	CompOp	—
map 📖	CompOp	84 math math: CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, CategoryTheory.Over.whiskerLeft_left, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc, AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion, comp_diagonal_assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map, TopCat.range_pullback_map, CategoryTheory.Limits.pullback_lift_diagonal_isPullback, CategoryTheory.Over.starPullbackIsoStar_hom_app_left, map_id, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_f, CategoryTheory.Limits.isPullback_map_snd_snd, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst, CategoryTheory.PreOneHypercover.inter_p₂, CategoryTheory.ShortComplex.SnakeInput.functorP_map, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc, CategoryTheory.Over.tensorHom_left, map_comp_assoc, CategoryTheory.Limits.pullback_map_diagonal_isPullback, map_comp, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, CategoryTheory.Over.whiskerRight_left, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_f, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc, comp_diagonal, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, CategoryTheory.MorphismProperty.pullback_map, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd, CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, diagonal_comp, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd, CategoryTheory.IsKernelPair.pullback, TopCat.pullback_map_isOpenEmbedding, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, TopCat.pullback_map_isEmbedding, CategoryTheory.Over.starPullbackIsoStar_inv_app_left, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, CategoryTheory.PreOneHypercover.inter_p₁, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd, CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv, congrHom_inv, CategoryTheory.PreOneHypercover.cylinder_p₁, CategoryTheory.PreOneHypercover.cylinder_p₂, congrHom_hom, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, map_isIso, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, CategoryTheory.Limits.pullbackFstFstIso_inv, CategoryTheory.Limits.pullback_lift_map_isPullback, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, CategoryTheory.PreOneHypercover.cylinder_Y, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
mapDesc 📖	CompOp	3 math math: AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme, AlgebraicGeometry.IsImmersion.instMapDescScheme, mapDesc_comp
snd 📖	CompOp	420 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, TopCat.isInducing_pullback_to_prod, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁, CategoryTheory.Over.associator_hom_left_snd_fst_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom_assoc, CategoryTheory.Over.prodLeftIsoPullback_hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_snd', AlgebraicGeometry.instLocallyQuasiFiniteSndScheme, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso, CategoryTheory.Limits.pullbackProdSndIsoProd_hom_snd, CategoryTheory.Over.associator_inv_left_snd, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc, CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, CategoryTheory.Limits.pullbackFstFstIso_hom, CategoryTheory.IsPullback.isoPullback_inv_snd_assoc, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc, CategoryTheory.Abelian.epi_pullback_of_epi_f, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf, CategoryTheory.MorphismProperty.pullback_snd_iff, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, diagonal_snd_assoc, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst, TopCat.snd_isOpenEmbedding_of_left, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_snd_of_left, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃_assoc, CategoryTheory.Limits.Concrete.pullbackMk_snd, AlgebraicGeometry.IsProper.instSndScheme, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc, CategoryTheory.Over.grpObjMkPullbackSnd_one, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr_assoc, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.PreOneHypercover.cylinderHom_h₁, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left, CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, CategoryTheory.Limits.pullback_snd_iso_of_left_iso, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_map, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_base_snd, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd_assoc, CategoryTheory.Limits.pullbackAssoc_inv_fst_snd, CategoryTheory.Over.prodLeftIsoPullback_inv_snd, CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd, AlgebraicGeometry.instGeometricallyReducedSndScheme, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc, CategoryTheory.Over.leftUnitor_hom_left, CategoryTheory.Over.isCommMonObj_mk_pullbackSnd, CategoryTheory.Over.tensorObj_ext_iff, TopCat.pullback_topology, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, AlgebraicGeometry.IsIntegralHom.instSndScheme, AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd, AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd, CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst, diagonal_snd, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, AlgebraicGeometry.instGeometricallyIntegralSndScheme, lift_snd, CategoryTheory.MonoOver.pullback_obj_arrow, CategoryTheory.Over.preservesTerminalIso_pullback, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, CategoryTheory.Over.prodLeftIsoPullback_inv_snd_assoc, CategoryTheory.Over.rightUnitor_inv_left_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd_assoc, CategoryTheory.Abelian.Pseudoelement.pseudo_pullback, AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base, comp_diagonal_assoc, AlgebraicGeometry.pullbackSpecIso_inv_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, AlgebraicGeometry.Etale.instSndScheme, CategoryTheory.Over.prodLeftIsoPullback_hom_snd, CategoryTheory.Limits.PreservesPullback.iso_inv_snd, HomotopicalAlgebra.PrepathObject.trans_p₁, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.Over.whiskerRight_left_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc, CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, CategoryTheory.MorphismProperty.baseChange_map', AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, CategoryTheory.IsPullback.isoPullback_inv_snd, CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd, TopCat.range_pullback_map, CategoryTheory.GlueData.t'_iji, CategoryTheory.Subobject.pullback_obj, AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd, lift_snd_assoc, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd, CategoryTheory.ShortComplex.SnakeInput.snd_δ, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.instIsClosedImmersionSndScheme, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, CategoryTheory.Over.tensorHom_left_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.specTensorTo_snd_assoc, CategoryTheory.Limits.PullbackCone.snd_limit_cone, CategoryTheory.Over.leftUnitor_inv_left_snd, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_snd', AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc, CategoryTheory.Over.μ_pullback_left_fst_snd', instIsSplitEpiSnd, AlgebraicGeometry.Scheme.Pullback.range_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_snd, AlgebraicGeometry.instGeometricallyIrreducibleSndScheme, CategoryTheory.Over.leftUnitor_inv_left_snd_assoc, exists_lift, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd, diagonal_isKernelPair, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd, CategoryTheory.GlueData.t_fac, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_right, CategoryTheory.regularTopology.mapToEqualizer_eq_comp, AlgebraicGeometry.UniversallyOpen.snd, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth, CategoryTheory.Limits.isPullback_map_snd_snd, CategoryTheory.PreZeroHypercover.pullback₂_f, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd_assoc, CategoryTheory.Over.associator_hom_left_snd_fst, CategoryTheory.Limits.PreservesPullback.iso_inv_snd_assoc, CategoryTheory.Over.rightUnitor_inv_left_snd_assoc, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd, AlgebraicGeometry.instQuasiCompactSndScheme, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, TopCat.pullbackIsoProdSubtype_inv_snd_apply, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left, CategoryTheory.Limits.pullbackAssoc_hom_snd_fst, AlgebraicGeometry.Scheme.Pullback.range_snd_comp, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst, CategoryTheory.Over.pullback_map_left, condition_assoc, CategoryTheory.PreZeroHypercover.interSnd_h₀, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_fst, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_snd_eq_p₃, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, CategoryTheory.GlueData.t_fac_assoc, CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd_assoc, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.Over.associator_inv_left_fst_snd, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd_assoc, CategoryTheory.Limits.hasPullback_assoc_symm, CategoryTheory.Over.associator_hom_left_snd_snd_assoc, TopCat.pullbackIsoProdSubtype_hom_snd, CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, TopCat.snd_iso_of_left_embedding_range_subset, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc, CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.Over.μ_pullback_left_fst_snd, CategoryTheory.Over.monObjMkPullbackSnd_one, TopCat.pullbackIsoProdSubtype_inv_snd, AlgebraicGeometry.instQuasiSeparatedSndScheme, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, AlgebraicGeometry.IsFinite.instSndScheme, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc, AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst, CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift, CategoryTheory.GlueData.t'_jii, prodIsoPullback_hom_snd, CategoryTheory.Regular.instHasCoequalizerFstSnd, CategoryTheory.Limits.PreservesPullback.iso_hom_snd_assoc, TopCat.range_pullback_to_prod, CategoryTheory.Presieve.pullback_singleton, TopCat.pullback_fst_image_snd_preimage, AlgebraicGeometry.Surjective.instSndScheme, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc, prodIsoPullback_hom_snd_assoc, AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc, CategoryTheory.Over.snd_left, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_snd, CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom, CategoryTheory.Over.whiskerRight_left_snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, CategoryTheory.Limits.pullbackComparison_comp_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc, CategoryTheory.regularTopology.equalizerCondition_w', AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, comp_diagonal, CategoryTheory.Limits.fst_eq_snd_of_mono_eq, snd_of_mono, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, CategoryTheory.Over.η_pullback_left, CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_fst_assoc, AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, hom_ext_iff, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, CategoryTheory.MonoOver.inf_map_app, CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd, CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso_assoc, CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop, CategoryTheory.instHasLiftingPropertySnd, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, TopCat.isEmbedding_pullback_to_prod, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, AlgebraicGeometry.Scheme.Pullback.range_snd, AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme, TopCat.pullbackIsoProdSubtype_hom_apply, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc, CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, CategoryTheory.instIsRegularEpiSnd, CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst, diagonal_comp, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc, CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst', CategoryTheory.Limits.pullbackObjIso_hom_comp_snd_assoc, CategoryTheory.Over.whiskerLeft_left_snd_assoc, CategoryTheory.Limits.Types.range_pullbackSnd, CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono, AlgebraicGeometry.IsPreimmersion.instSndScheme, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst, prodIsoPullback_inv_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd, CategoryTheory.Over.associator_inv_left_fst_snd_assoc, CategoryTheory.IsPullback.isoPullback_hom_snd_assoc, CategoryTheory.MorphismProperty.Over.pullback_map_left, CategoryTheory.Limits.pullbackProdSndIsoProd_hom_snd_assoc, CategoryTheory.Limits.pullbackComparison_comp_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, CategoryTheory.Over.μ_pullback_left_snd, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst_assoc, CategoryTheory.MorphismProperty.pullback_snd, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, CategoryTheory.GlueData'.t_fac, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr, CategoryTheory.Limits.pullbackObjIso_inv_comp_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst_assoc, CategoryTheory.MorphismProperty.Over.pullback_obj_hom, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj, HomotopicalAlgebra.instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, CategoryTheory.Limits.pullbackAssoc_hom_fst, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst, CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.canonicallyOverPullback_over, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd_assoc, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd, CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, CategoryTheory.Over.tensorHom_left_snd, CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd_assoc, AlgebraicGeometry.Flat.instSndScheme, CategoryTheory.Presieve.uncurry_pullbackArrows, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, prodIsoPullback_inv_snd_assoc, AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, condition, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_snd_assoc, CategoryTheory.IsPullback.isoPullback_hom_snd, CategoryTheory.IsKernelPair.of_hasPullback, AlgebraicGeometry.instSmoothSndScheme, CategoryTheory.Limits.mono_pullback_to_prod, CategoryTheory.PreOneHypercover.sieve₁_inter, CategoryTheory.Limits.pullbackProdSndIsoProd_inv_snd, AlgebraicGeometry.IsImmersion.instSndScheme, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd, CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv, HomotopicalAlgebra.instFibrationSndOfIsStableUnderBaseChangeFibrations, CategoryTheory.Limits.PreservesPullback.iso_hom_snd, AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, CategoryTheory.Limits.isIso_snd_of_mono, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd_assoc, CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, CategoryTheory.Over.isMonHom_pullbackFst_id_right, CategoryTheory.Over.pullback_obj_hom, AlgebraicGeometry.pullbackSpecIso_hom_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, CategoryTheory.Limits.pullbackAssoc_inv_snd, TopCat.pullback_snd_range, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr, CategoryTheory.Over.prodComparisonIso_pullback_inv_left_fst_snd', CategoryTheory.Functor.relativelyRepresentable.pullback₃.snd_fst'_eq_p₁_assoc, TopCat.snd_isEmbedding_of_left, CategoryTheory.Limits.pullbackObjIso_inv_comp_snd, CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc, CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc, CategoryTheory.Over.ε_pullback_left, lift_fst_snd, CategoryTheory.Limits.pullback_fst_map_snd_isPullback, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc, CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc, CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_assoc, CategoryTheory.Limits.pullbackProdFstIsoProd_hom_snd, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminal, CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst, CategoryTheory.Over.associator_hom_left_snd_snd, CategoryTheory.Over.associator_inv_left_snd_assoc, CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd, AlgebraicGeometry.IsSeparated.instSndScheme, AlgebraicGeometry.IsOpenImmersion.instSndScheme, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd_assoc, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, CategoryTheory.Limits.pullbackFstFstIso_inv, CategoryTheory.Over.whiskerLeft_left_snd, HomotopicalAlgebra.PathObject.trans_p₁, CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₂, CategoryTheory.Limits.diagonal_pullback_fst, TopCat.pullback_snd_image_fst_preimage, CategoryTheory.Limits.pullback_lift_map_isPullback, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, CategoryTheory.Limits.pullbackAssoc_inv_fst_fst, CategoryTheory.Limits.pullbackObjIso_hom_comp_snd, AlgebraicGeometry.universallyClosed_snd, CategoryTheory.Regular.instMonoDesc, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback fst snd	—	CategoryTheory.Limits.PullbackCone.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback fst snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
congrHom_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.pullback congrHom map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
congrHom_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.pullback congrHom map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
exists_lift 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Limits.pullback fst snd	—	CategoryTheory.Limits.limit.lift_π
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback fst snd	—	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.Limits.PullbackCone.equalizer_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback fst snd	—	hom_ext
lift_fst 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback lift fst	—	CategoryTheory.Limits.limit.lift_π
lift_fst_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback lift fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
lift_fst_snd 📖	mathematical	—	lift CategoryTheory.Limits.pullback fst snd condition CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext condition CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.id_comp
lift_snd 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback lift snd	—	CategoryTheory.Limits.limit.lift_π
lift_snd_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback lift snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_snd
mapDesc_comp 📖	mathematical	—	mapDesc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Iso.hom congrHom CategoryTheory.Category.assoc	—	CategoryTheory.Category.assoc hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id
map_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback map	—	hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc
map_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback	—	hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_isIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.Limits.pullback map	—	CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsIso.inv_hom_id

CategoryTheory.Limits.pushout

Definitions

Name	Category	Theorems
cocone 📖	CompOp	—
congrHom 📖	CompOp	3 math math: congrHom_hom, mapLift_comp, congrHom_inv
desc 📖	CompOp	15 math math: inr_desc, HomotopicalAlgebra.Precylinder.trans_π, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left, CategoryTheory.Under.pushout_map, inl_desc_assoc, CategoryTheory.Limits.pushoutComparison_map_desc, HomotopicalAlgebra.Cylinder.trans_π, HomotopicalAlgebra.Precylinder.LeftHomotopy.trans_h, desc_inl_inr, CategoryTheory.Limits.pushoutComparison_map_desc_assoc, CategoryTheory.Under.mapPushoutAdj_counit_app, inr_desc_assoc, inl_desc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_ι
inl 📖	CompOp	112 math math: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.instHasLiftingPropertyInl, CategoryTheory.Limits.hasPushout_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom, CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone, inl_coprodIsoPushout_hom, CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom_assoc, CategoryTheory.Limits.inl_comp_pushoutComparison_assoc, CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc, CategoryTheory.Limits.inl_comp_pushoutObjIso_hom, CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_left, CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc, CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom, condition, CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom, CategoryTheory.Limits.inl_comp_pushoutComparison, CategoryTheory.Under.pushout_map, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst, CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl, CategoryTheory.Limits.Types.instMonoPushoutInl, CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom, inl_desc_assoc, CategoryTheory.Limits.PreservesPushout.inl_iso_inv, CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst_assoc, CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc, CategoryTheory.Under.mapPushoutAdj_unit_app, CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, hom_ext_iff, CommRingCat.HomTopology.isEmbedding_pushout, CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso_assoc, CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst, CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst, inl_of_epi, CategoryTheory.Limits.inl_eq_inr_of_epi_eq, CategoryTheory.Abelian.mono_pushout_of_mono_g, CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_assoc, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst, CategoryTheory.Limits.inr_pushoutAssoc_hom, exists_desc, CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv, CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv, CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc, CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc, CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right, CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv, CategoryTheory.Limits.epi_coprod_to_pushout, CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi, CategoryTheory.MorphismProperty.pushout_inl, HomotopicalAlgebra.Cylinder.trans_i₀, CategoryTheory.IsPushout.inl_isoPushout_inv, CategoryTheory.Limits.inl_inl_pushoutAssoc_hom, HomotopicalAlgebra.instCofibrationInlOfIsStableUnderCobaseChangeCofibrations, AlgebraicGeometry.isPullback_Spec_map_pushout, CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom_assoc, CategoryTheory.Limits.inl_inr_pushoutAssoc_inv, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl, desc_inl_inr, CommRingCat.inl_injective_of_flat, CategoryTheory.Limits.inl_comp_pushoutObjIso_inv, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc, CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv, CategoryTheory.IsPushout.inl_isoPushout_hom, HomotopicalAlgebra.instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc, CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv_assoc, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl, CategoryTheory.Limits.inl_comp_pushoutObjIso_inv_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom_assoc, CategoryTheory.IsPushout.inl_isoPushout_hom_assoc, CategoryTheory.Limits.inr_inl_pushoutAssoc_hom, CategoryTheory.Limits.pushout_inl_iso_of_right_iso, CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_assoc, CategoryTheory.IsPushout.inl_isoPushout_inv_assoc, CategoryTheory.Limits.inl_comp_pushoutObjIso_hom_assoc, AlgebraicGeometry.isPullback_SpecMap_pushout, CategoryTheory.Limits.inl_pushoutAssoc_inv, CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc, CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom, CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc, inl_coprodIsoPushout_inv, CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv, CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom_assoc, CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso_assoc, CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc, CategoryTheory.Limits.PreservesPushout.inl_iso_hom, CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom, inl_desc, CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom_assoc, inl_coprodIsoPushout_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl_assoc, CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso, inl_coprodIsoPushout_inv_assoc, CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc, condition_assoc, CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso, CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv_assoc, HomotopicalAlgebra.Precylinder.trans_i₀, CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom, CategoryTheory.Limits.isIso_inl_of_epi, CategoryTheory.Limits.inr_inr_pushoutAssoc_inv, CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom, CategoryTheory.MorphismProperty.pushout_inl_iff, RingHom.IsStableUnderBaseChange.pushout_inl
inr 📖	CompOp	115 math math: CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom_assoc, CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.Limits.PreservesPushout.inr_iso_inv_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd, inr_desc, CategoryTheory.Limits.PreservesPushout.inr_iso_inv, CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom_assoc, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr_assoc, CategoryTheory.Limits.pushout_inr_iso_of_left_iso, CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc, CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom, CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc, CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom, CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc, CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc, CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc, CategoryTheory.Limits.inr_comp_pushoutObjIso_hom_assoc, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd, condition, CategoryTheory.Limits.inr_inl_pushoutRightPushoutInlIso_hom, CategoryTheory.Under.pushout_map, CategoryTheory.IsPushout.inr_isoPushout_inv_assoc, CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, CategoryTheory.IsPushout.inr_isoPushout_hom_assoc, CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom_assoc, CategoryTheory.IsPushout.inr_isoPushout_inv, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom, CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv_assoc, CategoryTheory.Limits.hasPushout_assoc_symm, CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom, CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc, CategoryTheory.Under.mapPushoutAdj_unit_app, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, hom_ext_iff, CommRingCat.HomTopology.isEmbedding_pushout, inr_coprodIsoPushout_hom_assoc, HomotopicalAlgebra.instCofibrationInrOfIsStableUnderCobaseChangeCofibrations, CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso_assoc, HomotopicalAlgebra.instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, CategoryTheory.Limits.inl_eq_inr_of_epi_eq, CommRingCat.inr_injective_of_flat, CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi, CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_assoc, CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.MorphismProperty.pushout_inr, CategoryTheory.Limits.inr_pushoutAssoc_hom, CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd, exists_desc, CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv, CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone, CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv, CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc, CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv, CategoryTheory.Limits.epi_coprod_to_pushout, CategoryTheory.Limits.PreservesPushout.inr_iso_hom, CategoryTheory.Limits.inl_inl_pushoutAssoc_hom, AlgebraicGeometry.isPullback_Spec_map_pushout, CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom, CategoryTheory.Limits.inl_inr_pushoutAssoc_inv, desc_inl_inr, CategoryTheory.instHasLiftingPropertyInr, CategoryTheory.Limits.inr_comp_pushoutObjIso_inv, CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv, CategoryTheory.Under.pushout_obj, CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv, CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc, CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv_assoc, inr_coprodIsoPushout_hom, CategoryTheory.Limits.inr_inl_pushoutAssoc_hom, CategoryTheory.MorphismProperty.pushout_inr_iff, CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_assoc, CategoryTheory.Limits.inr_comp_pushoutComparison_assoc, CategoryTheory.Under.mapPushoutAdj_counit_app, HomotopicalAlgebra.Cylinder.trans_i₁, AlgebraicGeometry.isPullback_SpecMap_pushout, CategoryTheory.Limits.inl_pushoutAssoc_inv, CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc, CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr, CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc, CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso_assoc, inr_desc_assoc, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right, CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr, CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc, CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd, CategoryTheory.Abelian.mono_pushout_of_mono_f, CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd_assoc, CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom, CategoryTheory.Limits.isIso_inr_of_epi, inr_coprodIsoPushout_inv, CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, CategoryTheory.Limits.inr_comp_pushoutObjIso_inv_assoc, CategoryTheory.Limits.Types.instMonoPushoutInr, CategoryTheory.Limits.inr_comp_pushoutObjIso_hom, CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom_assoc, CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso, CategoryTheory.IsPushout.inr_isoPushout_hom, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc, CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc, CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr, CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom, HomotopicalAlgebra.Precylinder.trans_i₁, inr_coprodIsoPushout_inv_assoc, condition_assoc, CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso, CategoryTheory.Limits.inr_inr_pushoutAssoc_inv, CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom, CategoryTheory.Limits.inr_comp_pushoutComparison, inr_of_epi, CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right
isColimit 📖	CompOp	—
map 📖	CompOp	6 math math: map_comp, map_comp_assoc, congrHom_hom, congrHom_inv, map_id, map_isIso
mapLift 📖	CompOp	1 math math: mapLift_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl inr	—	CategoryTheory.Limits.PushoutCocone.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl inr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
congrHom_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.pushout congrHom map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
congrHom_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.pushout congrHom map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp
desc_inl_inr 📖	mathematical	—	desc CategoryTheory.Limits.pushout inl inr condition CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	hom_ext condition CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.comp_id
exists_desc 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Limits.pushout inl inr	—	CategoryTheory.Limits.colimit.ι_desc
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl inr	—	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.PushoutCocone.coequalizer_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout inl inr	—	hom_ext
inl_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout inl desc	—	CategoryTheory.Limits.colimit.ι_desc
inl_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout inl desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_desc
inr_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout inr desc	—	CategoryTheory.Limits.colimit.ι_desc
inr_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout inr desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_desc
mapLift_comp 📖	mathematical	—	mapLift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout CategoryTheory.Iso.hom congrHom CategoryTheory.Category.assoc	—	CategoryTheory.Category.assoc hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.Limits.colimit.ι_desc_assoc
map_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout map	—	hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_desc
map_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pushout map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pushout	—	hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
map_isIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.Limits.pushout map	—	CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc hom_ext CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Category.comp_id

---

← Back to Index