Pullbacks

📁 Source: Mathlib/AlgebraicGeometry/Pullbacks.lean

Statistics

Metric	Count
Definitions GrpObjAsOverPullback, diagonalCover, diagonalCoverDiagonalRange, diagonalRestrictIsoDiagonal, fV, gluedIsLimit, gluedLift, gluedLiftPullbackMap, gluing, openCoverOfBase, openCoverOfBase', openCoverOfLeft, openCoverOfLeftRight, openCoverOfRight, p1, p2, pullbackFstιToV, pullbackP1Iso, t, t', v, canonicallyOverPullback, monObjAsOverPullback, instBraidedCategoryOverScheme, instCartesianMonoidalCategoryOverScheme, pullbackSpecIso	26
Theorems affine_affine_hasPullback, affine_hasPullback, base_affine_hasPullback, cocycle, cocycle_fst_fst_fst, cocycle_fst_fst_snd, cocycle_fst_snd, cocycle_snd_fst_fst, cocycle_snd_fst_snd, cocycle_snd_snd, diagonalCover_map, gluedLiftPullbackMap_fst, gluedLiftPullbackMap_fst_assoc, gluedLiftPullbackMap_snd, gluedLiftPullbackMap_snd_assoc, gluedLift_p1, gluedLift_p2, gluing_J, gluing_U, gluing_V, gluing_f, gluing_t, gluing_t', gluing_ι, hasPullback_of_cover, instHasPullback, instHasPullbacks, isAffine_of_isAffine_isAffine_isAffine, left_affine_comp_pullback_hasPullback, lift_comp_ι, openCoverOfBase'_f, openCoverOfBase_I₀, openCoverOfBase_X, openCoverOfBase_f, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X, openCoverOfLeftRight_f, openCoverOfLeft_I₀, openCoverOfLeft_X, openCoverOfLeft_f, openCoverOfRight_I₀, openCoverOfRight_X, openCoverOfRight_f, p_comm, pullbackFstιToV_fst, pullbackFstιToV_fst_assoc, pullbackFstιToV_snd, pullbackFstιToV_snd_assoc, pullbackP1Iso_hom_fst, pullbackP1Iso_hom_fst_assoc, pullbackP1Iso_hom_snd, pullbackP1Iso_hom_snd_assoc, pullbackP1Iso_hom_ι, pullbackP1Iso_hom_ι_assoc, pullbackP1Iso_inv_fst, pullbackP1Iso_inv_fst_assoc, pullbackP1Iso_inv_snd, pullbackP1Iso_inv_snd_assoc, t'_fst_fst_fst, t'_fst_fst_fst_assoc, t'_fst_fst_snd, t'_fst_fst_snd_assoc, t'_fst_snd, t'_fst_snd_assoc, t'_snd_fst_fst, t'_snd_fst_fst_assoc, t'_snd_fst_snd, t'_snd_fst_snd_assoc, t'_snd_snd, t'_snd_snd_assoc, t_fst_fst, t_fst_fst_assoc, t_fst_snd, t_fst_snd_assoc, t_id, t_snd, t_snd_assoc, canonicallyOverPullback_over, instIsOverFstOverInferInstanceOverClassId, isCommMonObj_asOver_pullback, isEmpty_pullback, isMonHom_fst_id_right, isPullback_of_openCover, monObjAsOverPullback_mul, monObjAsOverPullback_one, pullback_map_isOpenImmersion, diagonal_SpecMap, diagonal_Spec_map, isPullback_SpecMap_of_isPushout, isPullback_SpecMap_pushout, isPullback_Spec_map_isPushout, isPullback_Spec_map_pushout, pullbackSpecIso_hom_base, pullbackSpecIso_hom_base_assoc, pullbackSpecIso_hom_fst, pullbackSpecIso_hom_fst', pullbackSpecIso_hom_fst'_assoc, pullbackSpecIso_hom_fst_assoc, pullbackSpecIso_hom_snd, pullbackSpecIso_hom_snd_assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_fst', pullbackSpecIso_inv_fst'_assoc, pullbackSpecIso_inv_fst_assoc, pullbackSpecIso_inv_snd, pullbackSpecIso_inv_snd_assoc	106
Total	132

AlgebraicGeometry

Definitions

Name	Category	Theorems
instBraidedCategoryOverScheme 📖	CompOp	3 math math: isCommMonObj_of_isProper_of_geometricallyIntegral, Scheme.isCommMonObj_asOver_pullback, isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
instCartesianMonoidalCategoryOverScheme 📖	CompOp	7 math math: isCommMonObj_of_isProper_of_geometricallyIntegral, instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, Scheme.isCommMonObj_asOver_pullback, Scheme.isMonHom_fst_id_right, Scheme.monObjAsOverPullback_mul, Scheme.monObjAsOverPullback_one, isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
pullbackSpecIso 📖	CompOp	16 math math: diagonal_SpecMap, pullbackSpecIso_inv_snd, pullbackSpecIso_hom_base, pullbackSpecIso_inv_fst'_assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd_assoc, pullbackSpecIso_inv_fst_assoc, pullbackSpecIso_hom_fst, pullbackSpecIso_hom_base_assoc, pullbackSpecIso_hom_fst'_assoc, pullbackSpecIso_inv_fst', diagonal_Spec_map, pullbackSpecIso_hom_fst', pullbackSpecIso_hom_snd, pullbackSpecIso_hom_fst_assoc, pullbackSpecIso_hom_snd_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonal_SpecMap 📖	mathematical	—	CategoryTheory.Limits.pullback.diagonal Scheme Scheme.instCategory Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.lmul' CategoryTheory.Iso.inv NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing pullbackSpecIso	—	CategoryTheory.Limits.pullback.hom_ext Scheme.Pullback.instHasPullback AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.Limits.pullback.diagonal_fst CategoryTheory.Category.assoc pullbackSpecIso_inv_fst CommRingCat.hom_ext RingHom.ext mul_one CategoryTheory.Limits.pullback.diagonal_snd pullbackSpecIso_inv_snd one_mul
diagonal_Spec_map 📖	mathematical	—	CategoryTheory.Limits.pullback.diagonal Scheme Scheme.instCategory Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.lmul' CategoryTheory.Iso.inv NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing pullbackSpecIso	—	diagonal_SpecMap
isPullback_SpecMap_of_isPushout 📖	mathematical	CategoryTheory.IsPushout CommRingCat CommRingCat.instCategory	CategoryTheory.IsPullback Scheme Scheme.instCategory Spec Spec.map	—	CategoryTheory.IsPullback.map CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint CategoryTheory.IsPullback.flip CategoryTheory.IsPushout.op
isPullback_SpecMap_pushout 📖	mathematical	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Spec CategoryTheory.Limits.pushout CommRingCat CommRingCat.instCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span Spec.map CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr	—	isPullback_SpecMap_of_isPushout CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPushout.of_hasPushout
isPullback_Spec_map_isPushout 📖	mathematical	CategoryTheory.IsPushout CommRingCat CommRingCat.instCategory	CategoryTheory.IsPullback Scheme Scheme.instCategory Spec Spec.map	—	isPullback_SpecMap_of_isPushout
isPullback_Spec_map_pushout 📖	mathematical	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Spec CategoryTheory.Limits.pushout CommRingCat CommRingCat.instCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.span Spec.map CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr	—	isPullback_SpecMap_pushout
pullbackSpecIso_hom_base 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.instAlgebra CategoryTheory.Limits.pullback.fst	—	Scheme.Pullback.instHasPullback Spec.map_comp pullbackSpecIso_hom_fst_assoc
pullbackSpecIso_hom_base_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.instAlgebra CategoryTheory.Limits.pullback.fst	—	Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_hom_base
pullbackSpecIso_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.includeLeftRingHom CategoryTheory.Limits.pullback.fst	—	Scheme.Pullback.instHasPullback pullbackSpecIso_inv_fst CategoryTheory.Iso.hom_inv_id_assoc
pullbackSpecIso_hom_fst' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.Limits.pullback.fst	—	pullbackSpecIso_hom_fst
pullbackSpecIso_hom_fst'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.Limits.pullback.fst	—	Scheme.Pullback.instHasPullback Algebra.to_smulCommClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_hom_fst'
pullbackSpecIso_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso Algebra.TensorProduct.includeLeftRingHom CategoryTheory.Limits.pullback.fst	—	Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_hom_fst
pullbackSpecIso_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso RingHomClass.toRingHom AlgHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.includeRight CategoryTheory.Limits.pullback.snd	—	Scheme.Pullback.instHasPullback AlgHomClass.toRingHomClass AlgHom.algHomClass pullbackSpecIso_inv_snd CategoryTheory.Iso.hom_inv_id_assoc
pullbackSpecIso_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Spec CommRingCat.of Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Scheme.Pullback.instHasPullback TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing CategoryTheory.Iso.hom pullbackSpecIso RingHomClass.toRingHom AlgHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.includeRight CategoryTheory.Limits.pullback.snd	—	Scheme.Pullback.instHasPullback AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_hom_snd
pullbackSpecIso_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.fst Algebra.TensorProduct.includeLeftRingHom	—	CategoryTheory.Limits.limit.isoLimitCone_inv_π
pullbackSpecIso_inv_fst' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.fst Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	pullbackSpecIso_inv_fst
pullbackSpecIso_inv_fst'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.fst Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Scheme.Pullback.instHasPullback Algebra.to_smulCommClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_inv_fst'
pullbackSpecIso_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.fst Algebra.TensorProduct.includeLeftRingHom	—	Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_inv_fst
pullbackSpecIso_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.snd RingHomClass.toRingHom AlgHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.includeRight	—	CategoryTheory.Limits.limit.isoLimitCone_inv_π
pullbackSpecIso_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing CategoryTheory.Limits.pullback Spec.map CommRingCat.ofHom algebraMap Scheme.Pullback.instHasPullback CategoryTheory.Iso.inv pullbackSpecIso CategoryTheory.Limits.pullback.snd RingHomClass.toRingHom AlgHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.includeRight	—	Scheme.Pullback.instHasPullback AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackSpecIso_inv_snd

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
GrpObjAsOverPullback 📖	CompOp	—
canonicallyOverPullback 📖	CompOp	6 math math: isCommMonObj_asOver_pullback, isMonHom_fst_id_right, monObjAsOverPullback_mul, instIsOverFstOverInferInstanceOverClassId, canonicallyOverPullback_over, monObjAsOverPullback_one
monObjAsOverPullback 📖	CompOp	4 math math: isCommMonObj_asOver_pullback, isMonHom_fst_id_right, monObjAsOverPullback_mul, monObjAsOverPullback_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicallyOverPullback_over 📖	mathematical	—	CategoryTheory.over AlgebraicGeometry.Scheme instCategory CategoryTheory.Limits.pullback CategoryTheory.OverClass Pullback.instHasPullback CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback CategoryTheory.Limits.pullback.snd	—	Pullback.instHasPullback
instIsOverFstOverInferInstanceOverClassId 📖	mathematical	—	Hom.IsOver CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme instCategory CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Pullback.instHasPullback CategoryTheory.Limits.pullback.fst CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback	—	Pullback.instHasPullback CategoryTheory.Limits.pullback.condition CategoryTheory.Category.comp_id
isCommMonObj_asOver_pullback 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme AlgebraicGeometry.instBraidedCategoryOverScheme asOver CategoryTheory.Limits.pullback CategoryTheory.over CategoryTheory.OverClass Pullback.instHasPullback CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback monObjAsOverPullback	—	Pullback.instHasPullback CategoryTheory.Over.isCommMonObj_mk_pullbackSnd Pullback.instHasPullbacks
isEmpty_pullback 📖	mathematical	Disjoint Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	IsEmpty CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme instCategory Pullback.instHasPullback	—	isEmpty_of_commSq Pullback.instHasPullback CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.of_hasPullback
isMonHom_fst_id_right 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme CategoryTheory.OverClass.asOver CategoryTheory.Limits.pullback CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Pullback.instHasPullback CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback monObjAsOverPullback Hom.asOver CategoryTheory.Limits.pullback.fst instIsOverFstOverInferInstanceOverClassId	—	Pullback.instHasPullback instIsOverFstOverInferInstanceOverClassId CategoryTheory.Over.isMonHom_pullbackFst_id_right Pullback.instHasPullbacks
isPullback_of_openCover 📖	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange Pullback.instHasPullback CategoryTheory.PreZeroHypercover.f Cover.pullbackHom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange Pullback.instHasPullback Cover.hom_ext CategoryTheory.Limits.pullback.condition_assoc Cover.pullbackHom_map_assoc CategoryTheory.Category.assoc CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsPullback.paste_vert_iff CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.flip CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.IsPullback.isoPullback_hom_snd CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.isIso_hom CategoryTheory.MorphismProperty.of_zeroHypercover_target instHasPullbacksPrecoverageOfHasPullbacks instHasPullbacksIsOpenImmersion instIsLocalAtTargetIsomorphismsZariskiPrecoverage CategoryTheory.Precoverage.instSmallOfSmall instSmallPrecoverage CategoryTheory.IsPullback.of_iso_pullback
monObjAsOverPullback_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme asOver CategoryTheory.Limits.pullback CategoryTheory.over CategoryTheory.OverClass Pullback.instHasPullback CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback monObjAsOverPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Over.cartesianMonoidalCategory Pullback.instHasPullbacks CategoryTheory.Functor.obj CategoryTheory.Over.pullback CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.LaxBraided.toLaxMonoidal CategoryTheory.Over.braidedCategory CategoryTheory.Functor.Braided.toLaxBraided CategoryTheory.Over.instBraidedPullback CategoryTheory.Functor.map	—	Pullback.instHasPullbacks Pullback.instHasPullback
monObjAsOverPullback_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme asOver CategoryTheory.Limits.pullback CategoryTheory.over CategoryTheory.OverClass Pullback.instHasPullback CategoryTheory.CanonicallyOverClass.toOverClass canonicallyOverPullback monObjAsOverPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Over.cartesianMonoidalCategory Pullback.instHasPullbacks CategoryTheory.Functor.obj CategoryTheory.Over.pullback CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.LaxBraided.toLaxMonoidal CategoryTheory.Over.braidedCategory CategoryTheory.Functor.Braided.toLaxBraided CategoryTheory.Over.instBraidedPullback CategoryTheory.Functor.map	—	Pullback.instHasPullbacks Pullback.instHasPullback
pullback_map_isOpenImmersion 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback Pullback.instHasPullback CategoryTheory.Limits.pullback.map	—	Pullback.instHasPullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape Pullback.instHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv AlgebraicGeometry.IsOpenImmersion.instSndScheme AlgebraicGeometry.IsOpenImmersion.instFstScheme

AlgebraicGeometry.Scheme.Pullback

Definitions

Name	Category	Theorems
diagonalCover 📖	CompOp	1 math math: diagonalCover_map
diagonalCoverDiagonalRange 📖	CompOp	5 math math: AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index, diagonalCoverDiagonalRange_eq_top_of_injective, range_diagonal_subset_diagonalCoverDiagonalRange, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange
diagonalRestrictIsoDiagonal 📖	CompOp	—
fV 📖	CompOp	19 math math: t'_snd_fst_fst_assoc, cocycle, t'_fst_fst_snd_assoc, t'_snd_snd, t'_snd_fst_fst, t'_fst_fst_fst, cocycle_fst_fst_snd, cocycle_fst_fst_fst, t'_snd_fst_snd, cocycle_snd_fst_fst, t'_fst_fst_snd, cocycle_fst_snd, t'_snd_snd_assoc, t'_fst_snd_assoc, t'_fst_snd, t'_fst_fst_fst_assoc, cocycle_snd_snd, cocycle_snd_fst_snd, t'_snd_fst_snd_assoc
gluedIsLimit 📖	CompOp	—
gluedLift 📖	CompOp	2 math math: gluedLift_p1, gluedLift_p2
gluedLiftPullbackMap 📖	CompOp	4 math math: gluedLiftPullbackMap_snd, gluedLiftPullbackMap_snd_assoc, gluedLiftPullbackMap_fst_assoc, gluedLiftPullbackMap_fst
gluing 📖	CompOp	29 math math: gluedLiftPullbackMap_snd, gluedLiftPullbackMap_snd_assoc, gluedLift_p1, gluing_t, pullbackP1Iso_hom_snd, pullbackFstιToV_fst_assoc, gluedLift_p2, gluing_J, gluing_f, pullbackP1Iso_hom_fst_assoc, pullbackP1Iso_hom_ι_assoc, pullbackFstιToV_fst, pullbackP1Iso_inv_snd_assoc, pullbackP1Iso_inv_fst, pullbackP1Iso_inv_fst_assoc, gluing_U, pullbackP1Iso_hom_snd_assoc, gluing_ι, gluedLiftPullbackMap_fst_assoc, pullbackP1Iso_inv_snd, pullbackP1Iso_hom_ι, pullbackFstιToV_snd_assoc, pullbackFstιToV_snd, p_comm, gluing_t', pullbackP1Iso_hom_fst, lift_comp_ι, gluing_V, gluedLiftPullbackMap_fst
openCoverOfBase 📖	CompOp	4 math math: openCoverOfBase_I₀, openCoverOfBase_f, openCoverOfBase_X, diagonalCover_map
openCoverOfBase' 📖	CompOp	1 math math: openCoverOfBase'_f
openCoverOfLeft 📖	CompOp	3 math math: openCoverOfLeft_I₀, openCoverOfLeft_f, openCoverOfLeft_X
openCoverOfLeftRight 📖	CompOp	3 math math: openCoverOfLeftRight_f, openCoverOfLeftRight_I₀, openCoverOfLeftRight_X
openCoverOfRight 📖	CompOp	3 math math: openCoverOfRight_I₀, openCoverOfRight_f, openCoverOfRight_X
p1 📖	CompOp	17 math math: gluedLift_p1, pullbackP1Iso_hom_snd, pullbackFstιToV_fst_assoc, pullbackP1Iso_hom_fst_assoc, pullbackP1Iso_hom_ι_assoc, pullbackFstιToV_fst, pullbackP1Iso_inv_snd_assoc, pullbackP1Iso_inv_fst, pullbackP1Iso_inv_fst_assoc, pullbackP1Iso_hom_snd_assoc, pullbackP1Iso_inv_snd, pullbackP1Iso_hom_ι, pullbackFstιToV_snd_assoc, pullbackFstιToV_snd, p_comm, pullbackP1Iso_hom_fst, lift_comp_ι
p2 📖	CompOp	5 math math: pullbackP1Iso_hom_snd, gluedLift_p2, pullbackP1Iso_hom_snd_assoc, p_comm, lift_comp_ι
pullbackFstιToV 📖	CompOp	4 math math: pullbackFstιToV_fst_assoc, pullbackFstιToV_fst, pullbackFstιToV_snd_assoc, pullbackFstιToV_snd
pullbackP1Iso 📖	CompOp	10 math math: pullbackP1Iso_hom_snd, pullbackP1Iso_hom_fst_assoc, pullbackP1Iso_hom_ι_assoc, pullbackP1Iso_inv_snd_assoc, pullbackP1Iso_inv_fst, pullbackP1Iso_inv_fst_assoc, pullbackP1Iso_hom_snd_assoc, pullbackP1Iso_inv_snd, pullbackP1Iso_hom_ι, pullbackP1Iso_hom_fst
t 📖	CompOp	8 math math: t_fst_snd_assoc, gluing_t, t_snd, t_fst_fst, t_id, t_fst_snd, t_snd_assoc, t_fst_fst_assoc
t' 📖	CompOp	20 math math: t'_snd_fst_fst_assoc, cocycle, t'_fst_fst_snd_assoc, t'_snd_snd, t'_snd_fst_fst, t'_fst_fst_fst, cocycle_fst_fst_snd, cocycle_fst_fst_fst, t'_snd_fst_snd, cocycle_snd_fst_fst, t'_fst_fst_snd, cocycle_fst_snd, t'_snd_snd_assoc, t'_fst_snd_assoc, t'_fst_snd, t'_fst_fst_fst_assoc, cocycle_snd_snd, cocycle_snd_fst_snd, gluing_t', t'_snd_fst_snd_assoc
v 📖	CompOp	31 math math: t'_snd_fst_fst_assoc, t_fst_snd_assoc, cocycle, t'_fst_fst_snd_assoc, pullbackFstιToV_fst_assoc, t_snd, pullbackFstιToV_fst, t_fst_fst, t'_snd_snd, t'_snd_fst_fst, t'_fst_fst_fst, t_id, cocycle_fst_fst_snd, cocycle_fst_fst_fst, t_fst_snd, t'_snd_fst_snd, cocycle_snd_fst_fst, t'_fst_fst_snd, cocycle_fst_snd, t'_snd_snd_assoc, t'_fst_snd_assoc, pullbackFstιToV_snd_assoc, t'_fst_snd, pullbackFstιToV_snd, t'_fst_fst_fst_assoc, cocycle_snd_snd, t_snd_assoc, cocycle_snd_fst_snd, t_fst_fst_assoc, gluing_V, t'_snd_fst_snd_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affine_affine_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec	—	hasPullback_of_cover affine_hasPullback AlgebraicGeometry.Scheme.local_affine
affine_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec	—	AlgebraicGeometry.Spec.full CategoryTheory.Functor.map_preimage CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbacks_opposite CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint
base_affine_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec	—	CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_cover affine_affine_hasPullback AlgebraicGeometry.Scheme.local_affine
cocycle 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.id_comp CategoryTheory.Category.assoc cocycle_fst_fst_fst cocycle_fst_fst_snd cocycle_fst_snd cocycle_snd_fst_fst cocycle_snd_fst_snd cocycle_snd_snd
cocycle_fst_fst_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t'	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_fst_fst_fst t'_fst_snd t'_snd_snd
cocycle_fst_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_fst_fst_snd
cocycle_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_fst_snd t'_snd_snd t'_fst_fst_fst
cocycle_snd_fst_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_snd_fst_fst t'_fst_snd t'_snd_snd CategoryTheory.Limits.pullback.condition_assoc
cocycle_snd_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_snd_fst_snd CategoryTheory.Limits.pullback.condition_assoc
cocycle_snd_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF t'_snd_snd t'_fst_fst_fst t'_fst_snd
diagonalCover_map 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback.diagonalObj instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion diagonalCover CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Limits.pullback openCoverOfBase CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Cover.pullbackHom CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange instHasPullback CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc
gluedLiftPullbackMap_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.PullbackCone.fst AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.GlueData.J gluedLiftPullbackMap CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.PullbackCone.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.id_comp CategoryTheory.Limits.PullbackCone.condition	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.id_comp CategoryTheory.Limits.PullbackCone.condition CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
gluedLiftPullbackMap_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.PullbackCone.fst AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.GlueData.J gluedLiftPullbackMap CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id CategoryTheory.Limits.PullbackCone.snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.id_comp CategoryTheory.Limits.PullbackCone.condition	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Category.id_comp CategoryTheory.Limits.PullbackCone.condition CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedLiftPullbackMap_fst
gluedLiftPullbackMap_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.PullbackCone.fst AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.GlueData.J gluedLiftPullbackMap CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.PullbackCone.condition CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd
gluedLiftPullbackMap_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.PullbackCone.fst AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.GlueData.J gluedLiftPullbackMap CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedLiftPullbackMap_snd
gluedLift_p1 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.GlueData.glued gluing gluedLift p1 CategoryTheory.Limits.PullbackCone.fst	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued CategoryTheory.Limits.Multicoequalizer.hom_ext AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Limits.Multicoequalizer.π_desc_assoc CategoryTheory.Limits.PullbackCone.condition AlgebraicGeometry.Scheme.Cover.glueMorphisms.congr_simp AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
gluedLift_p2 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.GlueData.glued gluing gluedLift p2 CategoryTheory.Limits.PullbackCone.snd	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued CategoryTheory.Limits.Multicoequalizer.hom_ext AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Limits.Multicoequalizer.π_desc_assoc CategoryTheory.Limits.PullbackCone.condition AlgebraicGeometry.Scheme.Cover.glueMorphisms.congr_simp AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
gluing_J 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.J AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.PreZeroHypercover.I₀	—	—
gluing_U 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.Limits.pullback	—	—
gluing_V 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.V AlgebraicGeometry.Scheme.GlueData.toGlueData gluing v	—	—
gluing_f 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.f AlgebraicGeometry.Scheme.GlueData.toGlueData gluing CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback	—	—
gluing_t 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.t AlgebraicGeometry.Scheme.GlueData.toGlueData gluing t	—	—
gluing_t' 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.GlueData.t' AlgebraicGeometry.Scheme.GlueData.toGlueData gluing t'	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF
gluing_ι 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	AlgebraicGeometry.Scheme.GlueData.ι gluing CategoryTheory.Limits.Multicoequalizer.π CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.GlueData.diagram AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram	—	—
hasPullback_of_cover 📖	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	—	p_comm
instHasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	hasPullback_of_cover AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF left_affine_comp_pullback_hasPullback
instHasPullbacks 📖	mathematical	—	CategoryTheory.Limits.HasPullbacks AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan instHasPullback
isAffine_of_isAffine_isAffine_isAffine 📖	mathematical	—	AlgebraicGeometry.IsAffine CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback	—	AlgebraicGeometry.IsAffine.of_isIso instHasPullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbacks_opposite CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.toSpecΓ_naturality CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.pullback.map_isIso AlgebraicGeometry.IsAffine.affine CategoryTheory.Iso.isIso_inv AlgebraicGeometry.instIsAffineObjOppositeCommRingCatSchemeSpec
left_affine_comp_pullback_hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.affineCover AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.hasPullback_assoc_symm AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left CategoryTheory.Limits.hasPullbackVertPaste base_affine_hasPullback AlgebraicGeometry.Scheme.local_affine
lift_comp_ι 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst p2 AlgebraicGeometry.Scheme.GlueData.ι	—	AlgebraicGeometry.Scheme.Cover.hom_ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.GlueData.glue_condition gluing_f gluing_t CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc t_fst_fst CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion pullbackFstιToV_snd t_fst_snd CategoryTheory.Limits.pullback.lift_snd pullbackFstιToV_fst_assoc CategoryTheory.Limits.pullback.condition_assoc AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.pullback.condition pullbackFstιToV_fst
openCoverOfBase'_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfBase' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Limits.pullback.snd CategoryTheory.Iso.hom CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Iso.inv CategoryTheory.Limits.Cone.pt CategoryTheory.IsPullback.cone CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.IsPullback.isLimit CategoryTheory.Precoverage.ZeroHypercover.pullback₁ AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.pullback.map CategoryTheory.CategoryStruct.id	—	instHasPullback AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities AlgebraicGeometry.isOpenImmersion_isMultiplicative AlgebraicGeometry.isOpenImmersion_respectsIso CategoryTheory.Category.assoc
openCoverOfBase_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfBase	—	instHasPullback
openCoverOfBase_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfBase CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.snd	—	instHasPullback
openCoverOfBase_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfBase CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.X CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	instHasPullback
openCoverOfLeftRight_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeftRight	—	instHasPullback
openCoverOfLeftRight_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeftRight CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	instHasPullback
openCoverOfLeftRight_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeftRight CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	instHasPullback
openCoverOfLeft_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeft	—	instHasPullback
openCoverOfLeft_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	instHasPullback
openCoverOfLeft_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfLeft CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	instHasPullback
openCoverOfRight_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfRight	—	instHasPullback
openCoverOfRight_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	instHasPullback
openCoverOfRight_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfRight CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	instHasPullback
p_comm 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	AlgebraicGeometry.Scheme.GlueData.glued gluing p1 p2	—	CategoryTheory.Limits.Multicoequalizer.hom_ext AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition
pullbackFstιToV_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion v pullbackFstιToV CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
pullbackFstιToV_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion v pullbackFstιToV CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackFstιToV_fst
pullbackFstιToV_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion v pullbackFstιToV CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
pullbackFstιToV_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion v pullbackFstιToV CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackFstιToV_snd
pullbackP1Iso_hom_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.lift_fst
pullbackP1Iso_hom_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackP1Iso_hom_fst
pullbackP1Iso_hom_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst p2	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.lift_snd
pullbackP1Iso_hom_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst p2	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackP1Iso_hom_snd
pullbackP1Iso_hom_ι 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.multicoequalizer CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.GlueData.diagram AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.Multicoequalizer.π CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram gluing_ι pullbackP1Iso_inv_fst CategoryTheory.Iso.hom_inv_id_assoc
pullbackP1Iso_hom_ι_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.hom pullbackP1Iso CategoryTheory.Limits.multicoequalizer CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.Scheme.GlueData.toGlueData CategoryTheory.GlueData.diagram AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram CategoryTheory.Limits.Multicoequalizer.π CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackP1Iso_hom_ι
pullbackP1Iso_inv_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.inv pullbackP1Iso CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.lift_fst
pullbackP1Iso_inv_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.inv pullbackP1Iso CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.GlueData.ι	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackP1Iso_inv_fst
pullbackP1Iso_inv_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.inv pullbackP1Iso CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.lift_snd
pullbackP1Iso_inv_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.GlueData.glued gluing p1 AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Iso.inv pullbackP1Iso CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackP1Iso_inv_snd
t'_fst_fst_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc CategoryTheory.Limits.pullback.lift_fst_assoc t_fst_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
t'_fst_fst_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_fst_fst_fst
t'_fst_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc CategoryTheory.Limits.pullback.lift_fst_assoc t_fst_snd CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
t'_fst_fst_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_fst_fst_snd
t'_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd CategoryTheory.Limits.pullback.lift_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd
t'_fst_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_fst_snd
t'_snd_fst_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc CategoryTheory.Limits.pullback.lift_fst_assoc t_fst_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
t'_snd_fst_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_snd_fst_fst
t'_snd_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc CategoryTheory.Limits.pullback.lift_fst_assoc t_fst_snd CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
t'_snd_fst_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_snd_fst_snd
t'_snd_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc CategoryTheory.Limits.pullback.lift_fst_assoc t_snd CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
t'_snd_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	CategoryTheory.Limits.pullback v fV AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.instIsOpenImmersionF t' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t'_snd_snd
t_fst_fst 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackAssoc_hom_snd_fst CategoryTheory.Limits.pullback.lift_fst_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd CategoryTheory.Limits.pullbackAssoc_inv_fst_fst CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
t_fst_fst_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t_fst_fst
t_fst_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackAssoc_hom_snd_snd CategoryTheory.Limits.pullback.lift_snd CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackAssoc_inv_snd CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
t_fst_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t_fst_snd
t_id 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	t CategoryTheory.CategoryStruct.id v	—	CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.id_comp CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc t_fst_fst CategoryTheory.Limits.pullback.condition t_fst_snd t_snd
t_snd 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd CategoryTheory.Limits.pullbackAssoc_hom_fst CategoryTheory.Limits.pullback.lift_fst_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst CategoryTheory.Limits.pullbackAssoc_inv_fst_snd CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
t_snd_assoc 📖	mathematical	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	v t CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' t_snd

---

← Back to Index