Preorder

📁 Source: Mathlib/CategoryTheory/Category/Preorder.lean

Statistics

Metric	Count
Definitions toOrderIso, toOrderHom, homOfLE, opHomOfLE, orderDualEquivalence, uniqueFromBot, uniqueToTop, hom, functor, equivFunctor, equivalenceFunctor, toFunctor, equivalence, smallCategory, le	15
Theorems toOrderIso_apply, toOrderIso_symm_apply, monotone, toOrderHom_coe, to_eq, eqToHom_comp_homOfLE, eqToHom_comp_homOfLE_assoc, eqToHom_comp_homOfLE_op, eqToHom_comp_homOfLE_op_assoc, homOfLE_comp, homOfLE_comp_eqToHom, homOfLE_comp_eqToHom_assoc, homOfLE_isIso_of_eq, homOfLE_leOfHom, homOfLE_op_comp_eqToHom, homOfLE_op_comp_eqToHom_assoc, homOfLE_refl, isIso_homOfLE, leOfHom, le_of_op_hom, orderDualEquivalence_counitIso, orderDualEquivalence_functor_map, orderDualEquivalence_functor_obj, orderDualEquivalence_inverse_map, orderDualEquivalence_inverse_obj, orderDualEquivalence_unitIso, functor_obj, equivFunctor_apply, equivFunctor_symm_apply, equivalenceFunctor_counitIso_hom_app_app, equivalenceFunctor_counitIso_inv_app_app, equivalenceFunctor_functor_obj_obj, equivalenceFunctor_inverse_obj, equivalenceFunctor_unitIso_hom_app, equivalenceFunctor_unitIso_inv_app, equivalence_counitIso, equivalence_functor, equivalence_inverse, equivalence_unitIso, isIso_iff_eq, subsingleton_hom, instFullFunctor	42
Total	57

CategoryTheory

Definitions

Name	Category	Theorems
homOfLE 📖	CompOp	255 math math: AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id, LightProfinite.proj_comp_transitionMap, Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, TopCat.Sheaf.interUnionPullbackCone_snd, Triangulated.TStructure.triangleω₁δ_obj_mor₁, SmallObject.SuccStruct.extendToSucc_map_le_succ, isIso_homOfLE, TopCat.Presheaf.germ_eq_of_isBasis, eqToHom_comp_homOfLE_op, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, Lattice.BicartSq.commSq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp_assoc, Functor.WellOrderInductionData.map_succ, Functor.WellOrderInductionData.Extension.ofLE_val, AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE, ThinSkeleton.map_map, Abelian.SpectralObject.SpectralSequence.HomologyData.kf_w, Functor.WellOrderInductionData.Extension.map_zero, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map, SmallObject.SuccStruct.arrowMk_iterationFunctor_map, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le', Triangulated.TStructure.triangleω₁δ_map_hom₁, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, TopCat.Sheaf.interUnionPullbackCone_fst, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TransfiniteCompositionOfShape.iic_isoBot, Triangulated.TStructure.ω₁δ_naturality_assoc, SmallObject.SuccStruct.ofCocone_map_assoc, HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, Triangulated.TStructure.triangleω₁δ_map_hom₂, Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, homOfLE_comp_eqToHom, Functor.ofSequence_map_homOfLE_succ, Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le', TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, OrderHom.equivalenceFunctor_counitIso_inv_app_app, SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_f, Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀', OrthogonalReflection.iteration_map_succ, AlgebraicGeometry.Scheme.ofRestrict_appLE, Abelian.SpectralObject.IsFirstQuadrant.isZero₂, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp, homOfLE_op_comp_eqToHom_assoc, TopologicalSpace.Opens.map_homOfLE, SmallObject.SuccStruct.extendToSucc.map_eq, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, TopCat.Presheaf.pullbackObjObjOfImageOpen_hom_naturality, SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality, TransfiniteCompositionOfShape.iic_isColimit, Subfunctor.equivalenceMonoOver_inverse_map, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, Triangulated.SpectralObject.ω₂_map_hom₁, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, Limits.CompleteLattice.finiteColimitCocone_cocone_ι_app, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, Limits.SequentialProduct.functorMap_commSq_aux, Limits.CompleteLattice.colimitCocone_cocone_ι_app, CompleteLattice.MulticoequalizerDiagram.multispanIndex_fst, SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, Triangulated.TStructure.triangleω₁δ_map_hom₃, PrincipalSeg.cocone_ι_app, SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality, ComposableArrows.opEquivalence_functor_obj_map, Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc, Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, ComposableArrows.δ₀Functor_obj_map, SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id, TopCat.Sheaf.interUnionPullbackConeLift_right, Limits.CompleteLattice.limitCone_isLimit_lift, TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left, toThinSkeleton_map, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, Limits.CompleteLattice.finiteLimitCone_isLimit_lift, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, SmallObject.SuccStruct.iterationFunctor_map_succ_assoc, AlgebraicGeometry.Scheme.zeroLocus_map, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.Scheme.homOfLE_appTop, SmallObject.ιFunctorObj_eq, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, Abelian.SpectralObject.IsFirstQuadrant.isZero₁, Abelian.SpectralObject.IsThirdQuadrant.isZero₂, Functor.ofOpSequence_map_homOfLE_succ, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, TransfiniteCompositionOfShape.iic_F, Functor.WellOrderInductionData.Extension.map_succ, Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id, AlgebraicGeometry.Scheme.Opens.ι_appTop, TopologicalSpace.Opens.overEquivalence_counitIso_inv_app, SmallObject.restrictionLE_map, OrthogonalReflection.iteration_map_succ_assoc, Triangulated.SpectralObject.ω₂_obj_mor₂, Preorder.coconeOfUpperBound_ι_app, Types.monoOverEquivalenceSet_functor_map, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left, SmallObject.SuccStruct.iterationFunctor_map_succ, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc, Limits.Types.isPushout_of_bicartSq, TopCat.Presheaf.pullback_obj_obj_ext_iff, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, eqToHom_comp_homOfLE, HasLiftingProperty.transfiniteComposition.SqStruct.sq, TopCat.Sheaf.interUnionPullbackConeLift_left, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.kerFunctor_map, OrthogonalReflection.iteration_map_succ_injectivity, Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_assoc, AlgebraicGeometry.Scheme.homOfLE_appLE, Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc, SmallObject.SuccStruct.Iteration.mapObj_refl, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, SmallObject.SuccStruct.ofCocone_map_to_top, Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀', orderDualEquivalence_counitIso, CompleteLattice.MulticoequalizerDiagram.multispanIndex_snd, AlgebraicGeometry.Scheme.toOpen_eq, SmallObject.SuccStruct.prop_iterationFunctor_map_succ, SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, OrderHom.equivalenceFunctor_counitIso_hom_app_app, Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, AlgebraicGeometry.Scheme.directedAffineCover_trans, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, TopCat.Presheaf.restrictOpenCommRingCat_apply, Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id, homOfLE_comp, MorphismProperty.TransfiniteCompositionOfShape.map_mem, SmallObject.SuccStruct.extendToSucc_map, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, Subfunctor.equivalenceMonoOver_unitIso, Abelian.SpectralObject.SpectralSequence.pageD_eq, orderDualEquivalence_functor_map, Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀', TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.Proj.awayMap_awayToSection, homOfLE_op_comp_eqToHom, TransfiniteCompositionOfShape.iic_incl_app, Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', Triangulated.TStructure.ω₁δ_app, Preorder.coneOfLowerBound_π_app, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, SmallObject.SuccStruct.Iteration.congr_map, Functor.WellOrderInductionData.Extension.compatibility, AlgebraicGeometry.Scheme.restrict_presheaf_map, TopCat.Sheaf.eq_app_of_locally_eq, SmallObject.SuccStruct.arrowMap_ofCocone, Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀', TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le, AlgebraicGeometry.Scheme.fromSpecStalk_app, Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_X₁, Functor.WellOrderInductionData.map_lift, Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀', AlgebraicGeometry.Scheme.homOfLE_base, HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc, Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app, homOfLE_isIso_of_eq, Types.monoOverEquivalenceSet_unitIso, Triangulated.SpectralObject.ω₂_map_hom₂, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, AlgebraicGeometry.Scheme.Opens.ι_appLE, SmallObject.restrictionLT_map, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, SmallObject.SuccStruct.ofCocone_map, AlgebraicGeometry.Scheme.appLE_comp_appLE, Triangulated.SpectralObject.ω₂_obj_obj₂, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, AlgebraicGeometry.Scheme.Opens.ι_app, Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁', SmallObject.prop_iterationFunctor_map_succ, eqToHom_comp_homOfLE_op_assoc, Limits.CompleteLattice.limitCone_cone_π_app, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, LightProfinite.proj_comp_transitionMapLE, homOfLE_comp_eqToHom_assoc, SmallObject.coconeOfLE_ι_app, Limits.SequentialProduct.functorMap_commSq_succ, Functor.WellOrderInductionData.Extension.map_limit, Triangulated.TStructure.triangleω₁δ_obj_mor₂, OrthogonalReflection.iteration_map_succ_surjectivity, Triangulated.SpectralObject.ω₂_obj_mor₁, HasLiftingProperty.transfiniteComposition.SqStruct.w₁, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, Triangulated.SpectralObject.ω₂_map_hom₃, Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃', Triangulated.TStructure.ω₁δ_naturality, TopologicalSpace.Opens.overEquivalence_counitIso_hom_app, Limits.CompleteLattice.colimitCocone_isColimit_desc, Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, TopCat.Sheaf.interUnionPullbackCone_pt, Limits.CompleteLattice.finiteLimitCone_cone_π_app, Types.monoOverEquivalenceSet_counitIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, SmallObject.SuccStruct.Iteration.prop_map_succ, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, Triangulated.SpectralObject.ω₂_obj_obj₁, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, HasLiftingProperty.transfiniteComposition.SqStruct.w₁_assoc, Abelian.SpectralObject.IsThirdQuadrant.isZero₁, Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom, Fin.succFunctor_map, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, orderDualEquivalence_inverse_map, Alexandrov.projSup_map, Subfunctor.equivalenceMonoOver_counitIso, Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le, Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, Topology.IsInducing.functor_map, Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc, Abelian.SpectralObject.isoMapFourδ₄Toδ₃'_hom, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, Limits.SequentialProduct.functorMap_commSq, Triangulated.SpectralObject.ω₂_obj_obj₃, Triangulated.TStructure.eTruncLT_map_eq_truncLTι, Triangulated.TStructure.spectralObject_δ, eqToHom_comp_homOfLE_assoc
opHomOfLE 📖	CompOp	—
orderDualEquivalence 📖	CompOp	13 math math: ComposableArrows.opEquivalence_counitIso_inv_app_app, orderDualEquivalence_unitIso, ComposableArrows.opEquivalence_unitIso_inv_app, ComposableArrows.opEquivalence_functor_map_app, ComposableArrows.opEquivalence_inverse_obj, ComposableArrows.opEquivalence_unitIso_hom_app, orderDualEquivalence_counitIso, orderDualEquivalence_functor_obj, orderDualEquivalence_functor_map, ComposableArrows.opEquivalence_inverse_map, orderDualEquivalence_inverse_obj, ComposableArrows.opEquivalence_counitIso_hom_app_app, orderDualEquivalence_inverse_map
uniqueFromBot 📖	CompOp	—
uniqueToTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom_comp_homOfLE 📖	mathematical	Preorder.toLE	CategoryStruct.comp Category.toCategoryStruct Preorder.smallCategory eqToHom homOfLE LE.le.trans le_of_eq	—	—
eqToHom_comp_homOfLE_assoc 📖	mathematical	Preorder.toLE	CategoryStruct.comp Category.toCategoryStruct Preorder.smallCategory eqToHom homOfLE LE.le.trans le_of_eq	—	LE.le.trans le_of_eq Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_comp_homOfLE
eqToHom_comp_homOfLE_op 📖	mathematical	Opposite.op Preorder.toLE	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Preorder.smallCategory Opposite.op eqToHom Quiver.Hom.op CategoryStruct.toQuiver homOfLE LE.le.trans le_of_eq Opposite.op_injective	—	—
eqToHom_comp_homOfLE_op_assoc 📖	mathematical	Opposite.op Preorder.toLE	CategoryStruct.comp Opposite Category.toCategoryStruct Category.opposite Preorder.smallCategory Opposite.op eqToHom CategoryStruct.opposite Quiver.Hom.op CategoryStruct.toQuiver homOfLE LE.le.trans le_of_eq Opposite.op_injective	—	LE.le.trans le_of_eq Opposite.op_injective Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eqToHom_comp_homOfLE_op
homOfLE_comp 📖	mathematical	Preorder.toLE	CategoryStruct.comp Category.toCategoryStruct Preorder.smallCategory homOfLE LE.le.trans	—	—
homOfLE_comp_eqToHom 📖	mathematical	Preorder.toLE	CategoryStruct.comp Category.toCategoryStruct Preorder.smallCategory homOfLE eqToHom LE.le.trans le_of_eq	—	—
homOfLE_comp_eqToHom_assoc 📖	mathematical	Preorder.toLE	CategoryStruct.comp Category.toCategoryStruct Preorder.smallCategory homOfLE eqToHom LE.le.trans le_of_eq	—	LE.le.trans le_of_eq Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_comp_eqToHom
homOfLE_isIso_of_eq 📖	mathematical	Preorder.toLE	IsIso Preorder.smallCategory homOfLE	—	le_of_eq
homOfLE_leOfHom 📖	mathematical	—	LE.le.hom Quiver.Hom.le	—	—
homOfLE_op_comp_eqToHom 📖	mathematical	Preorder.toLE Opposite.op	CategoryStruct.comp Opposite CategoryStruct.opposite Category.toCategoryStruct Preorder.smallCategory Opposite.op Quiver.Hom.op CategoryStruct.toQuiver homOfLE eqToHom LE.le.trans le_of_eq Opposite.op_injective	—	—
homOfLE_op_comp_eqToHom_assoc 📖	mathematical	Preorder.toLE Opposite.op	CategoryStruct.comp Opposite Category.toCategoryStruct Category.opposite Preorder.smallCategory Opposite.op Quiver.Hom.op CategoryStruct.toQuiver homOfLE eqToHom CategoryStruct.opposite LE.le.trans le_of_eq Opposite.op_injective	—	LE.le.trans le_of_eq Opposite.op_injective Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_op_comp_eqToHom
homOfLE_refl 📖	mathematical	Preorder.toLE	LE.le.hom CategoryStruct.id Category.toCategoryStruct Preorder.smallCategory	—	—
isIso_homOfLE 📖	mathematical	—	IsIso Preorder.smallCategory homOfLE	—	IsIso.id
leOfHom 📖	mathematical	—	Preorder.toLE	—	—
le_of_op_hom 📖	mathematical	—	Preorder.toLE Opposite.unop	—	—
orderDualEquivalence_counitIso 📖	mathematical	—	Equivalence.counitIso OrderDual Opposite Preorder.smallCategory OrderDual.instPreorder Category.opposite orderDualEquivalence Iso.refl Functor Functor.category Functor.comp DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Opposite.unop homOfLE Opposite.op OrderDual.ofDual Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct	—	—
orderDualEquivalence_functor_map 📖	mathematical	—	Functor.map OrderDual Preorder.smallCategory OrderDual.instPreorder Opposite Category.opposite Equivalence.functor orderDualEquivalence Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct homOfLE	—	—
orderDualEquivalence_functor_obj 📖	mathematical	—	Functor.obj OrderDual Preorder.smallCategory OrderDual.instPreorder Opposite Category.opposite Equivalence.functor orderDualEquivalence Opposite.op DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	—
orderDualEquivalence_inverse_map 📖	mathematical	—	Functor.map Opposite Category.opposite Preorder.smallCategory OrderDual OrderDual.instPreorder Equivalence.inverse orderDualEquivalence homOfLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Opposite.unop	—	—
orderDualEquivalence_inverse_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite Preorder.smallCategory OrderDual OrderDual.instPreorder Equivalence.inverse orderDualEquivalence DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Opposite.unop	—	—
orderDualEquivalence_unitIso 📖	mathematical	—	Equivalence.unitIso OrderDual Opposite Preorder.smallCategory OrderDual.instPreorder Category.opposite orderDualEquivalence Iso.refl Functor Functor.category Functor.id	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
toOrderIso 📖	CompOp	2 math math: toOrderIso_apply, toOrderIso_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toOrderIso_apply 📖	mathematical	—	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso toOrderIso CategoryTheory.Functor.obj Preorder.smallCategory functor	—	—
toOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso OrderIso.symm toOrderIso CategoryTheory.Functor.obj Preorder.smallCategory inverse	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
toOrderHom 📖	CompOp	5 math math: toOrderHom_coe, OrderHom.equivalenceFunctor_counitIso_inv_app_app, OrderHom.equivalenceFunctor_counitIso_hom_app_app, OrderHom.equivalenceFunctor_inverse_obj, OrderHom.equivFunctor_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monotone 📖	mathematical	—	Monotone obj Preorder.smallCategory	—	—
toOrderHom_coe 📖	mathematical	—	DFunLike.coe OrderHom OrderHom.instFunLike toOrderHom obj Preorder.smallCategory	—	—

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_eq 📖	—	—	—	—	le_antisymm

LE.le

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: AlgebraicGeometry.Scheme.Hom.resLE_map_assoc, AlgebraicGeometry.StructureSheaf.exists_const, AlgebraicGeometry.Scheme.Hom.resLE_map, Alexandrov.principals_map, CategoryTheory.homOfLE_refl, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.exists_lift_of_germInjective

Monotone

Definitions

Name	Category	Theorems
functor 📖	CompOp	40 math math: CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, OrderIso.equivalence_functor, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, CategoryTheory.TransfiniteCompositionOfShape.ici_F, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, instFullFunctor, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, PrincipalSeg.cocone_ι_app, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, final_functor_iff, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, PrincipalSeg.cocone_pt, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, OrderIso.equivalence_counitIso, CategoryTheory.TransfiniteCompositionOfShape.iic_F, CategoryTheory.SmallObject.restrictionLE_map, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, HasCardinalLT.Set.cocone_ι_app, HasCardinalLT.Set.functor_map_coe, OrderIso.equivalence_inverse, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, functor_obj, preordToCat_map, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, CategoryTheory.Functor.WellOrderInductionData.map_lift, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, CategoryTheory.SmallObject.restrictionLT_map, Set.Ici.subtype_functor_final, CategoryTheory.SmallObject.coconeOfLE_ι_app, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, SimplexCategory.toCat_map, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, OrderIso.equivalence_unitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_obj 📖	mathematical	Monotone	CategoryTheory.Functor.obj Preorder.smallCategory functor	—	—

OrderHom

Definitions

Name	Category	Theorems
equivFunctor 📖	CompOp	2 math math: equivFunctor_apply, equivFunctor_symm_apply
equivalenceFunctor 📖	CompOp	6 math math: equivalenceFunctor_counitIso_inv_app_app, equivalenceFunctor_functor_obj_obj, equivalenceFunctor_counitIso_hom_app_app, equivalenceFunctor_unitIso_hom_app, equivalenceFunctor_inverse_obj, equivalenceFunctor_unitIso_inv_app
toFunctor 📖	CompOp	3 math math: equivalenceFunctor_counitIso_inv_app_app, equivFunctor_apply, equivalenceFunctor_counitIso_hom_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivFunctor_apply 📖	mathematical	—	DFunLike.coe Equiv OrderHom CategoryTheory.Functor Preorder.smallCategory EquivLike.toFunLike Equiv.instEquivLike equivFunctor toFunctor	—	—
equivFunctor_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor Preorder.smallCategory OrderHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFunctor CategoryTheory.Functor.toOrderHom	—	—
equivalenceFunctor_counitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp OrderHom instPreorder CategoryTheory.Functor.toOrderHom CategoryTheory.homOfLE toFunctor CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso equivalenceFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivalenceFunctor_counitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp OrderHom instPreorder CategoryTheory.Functor.toOrderHom CategoryTheory.homOfLE toFunctor CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso equivalenceFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivalenceFunctor_functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory OrderHom instPreorder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor equivalenceFunctor DFunLike.coe instFunLike	—	—
equivalenceFunctor_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Preorder.smallCategory CategoryTheory.Functor.category OrderHom instPreorder CategoryTheory.Equivalence.inverse equivalenceFunctor CategoryTheory.Functor.toOrderHom	—	—
equivalenceFunctor_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app OrderHom Preorder.smallCategory instPreorder CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso equivalenceFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivalenceFunctor_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app OrderHom Preorder.smallCategory instPreorder CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso equivalenceFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

OrderIso

Definitions

Name	Category	Theorems
equivalence 📖	CompOp	14 math math: CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, equivalence_functor, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, equivalence_counitIso, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot, CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence, equivalence_inverse, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isColimit, equivalence_unitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Preorder.smallCategory equivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso symm monotone CategoryTheory.Functor.id CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	monotone
equivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Preorder.smallCategory equivalence Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso monotone	—	—
equivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Preorder.smallCategory equivalence Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso symm	—	—
equivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Preorder.smallCategory equivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso monotone symm CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	monotone

PartialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_iff_eq 📖	mathematical	—	CategoryTheory.IsIso Preorder.smallCategory toPreorder	—	CategoryTheory.Iso.to_eq Preorder.subsingleton_hom CategoryTheory.IsIso.id

Preorder

Definitions

Name	Category	Theorems
smallCategory 📖	CompOp	2702 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, TopologicalSpace.OpenNhds.coe_id, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app, SSet.OneTruncation₂.nerveEquiv_apply, CategoryTheory.Triangulated.SpectralObject.Hom.comm, AlgebraicGeometry.Scheme.toSpecΓ_apply, HomotopyCategory.spectralObjectMappingCone_δ'_app, AlgebraicGeometry.Scheme.Hom.resLE_map_assoc, CategoryTheory.Classifier.pullback_χ_obj_mk_truth, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc, AlgebraicGeometry.Γ_map_morphismRestrict, CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc, smoothSheafCommRing.ι_forgetStalk_inv, CategoryTheory.Subobject.map_mk, CategoryTheory.Abelian.SpectralObject.exact₁', AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_zero, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, ModuleCat.directLimitDiagram_obj_isModule, CategoryTheory.Limits.imageSubobject_arrow_assoc, CategoryTheory.Subobject.factorThru_right, CategoryTheory.ComposableArrows.isoMk₁_hom_app, TopCat.PrelocalPredicate.res, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id, CategoryTheory.Subobject.factors_iff, TopologicalSpace.Opens.id_apply, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow, CategoryTheory.ComposableArrows.exact_iff_δlast, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, CategoryTheory.ComposableArrows.sc'MapIso_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, LightProfinite.proj_comp_transitionMap, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, TopologicalSpace.Opens.map_id_obj_unop, LightProfinite.Extend.functorOp_obj, AlgebraicGeometry.Scheme.zeroLocus_iInf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, AlgebraicGeometry.IsAffineOpen.map_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, TopologicalSpace.Opens.inclusion'_hom_apply, CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles, Set.functorToTypes_obj, AlgebraicGeometry.Etale.etale_appLE, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.LocallyQuasiFinite.quasiFinite_appLE, TopCat.presheafToType_map, TopCat.Sheaf.interUnionPullbackCone_snd, TopologicalSpace.Opens.map_coe, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, CategoryTheory.NatTrans.ofOpSequence_app, CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_H, CategoryTheory.Subobject.imageFactorisation_F_m, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, CategoryTheory.nerve.σ_obj, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, CategoryTheory.Subobject.underlyingIso_arrow_assoc, AlgebraicGeometry.Scheme.IsQuasiAffine.toIsImmersion, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, CategoryTheory.ShortComplex.mapToComposableArrows_app_0, CategoryTheory.Subobject.hasColimitsOfSize, CategoryTheory.ComposableArrows.IsComplex.zero'_assoc, AlgebraicGeometry.Scheme.ofRestrict_appIso, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_π, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc, CategoryTheory.Limits.hasLimitsOfSize_thinSkeleton, AlgebraicGeometry.RingedSpace.basicOpen_res, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, CategoryTheory.Pairwise.diagram_obj, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc, CategoryTheory.isIso_homOfLE, AlgebraicGeometry.opensCone_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, Topology.IsOpenEmbedding.functor_isContinuous, SSet.horn₃₁.desc.multicofork_π_two, AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset, AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ, AlgebraicGeometry.mono_pushoutSection_of_iSup_eq, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.StructureSheaf.comap_id, RingHom.IsStableUnderBaseChange.pullback_fst_appTop, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, TopCat.Presheaf.germ_eq_of_isBasis, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, CategoryTheory.ComposableArrows.isIso_iff₂, CategoryTheory.Abelian.SpectralObject.zero₂_assoc, CategoryTheory.Dial.tensorObjImpl_rel, AlgebraicGeometry.IsAffineOpen.map_fromSpec, IsOpenMap.pullbackIso_hom_app_app, AlgebraicGeometry.StructureSheaf.const_mul_rev, CategoryTheory.eqToHom_comp_homOfLE_op, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, TopCat.Presheaf.Pushforward.id_inv_app, CategoryTheory.isCofilteredOrEmpty_of_directed_ge, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₁, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_zero, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁, TopCat.Presheaf.germ_stalkPullbackHom, CategoryTheory.orderDualEquivalence_unitIso, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, Lattice.BicartSq.commSq, skyscraperPresheaf_obj, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app, imageToKernel_unop, CategoryTheory.nerve.δ₂_zero, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, CategoryTheory.Abelian.SpectralObject.instMonoFromOpcycles, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, CategoryTheory.GrothendieckTopology.diagram_obj, AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, AlgebraicGeometry.StructureSheaf.comap_comp, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.morphismRestrict_ι_assoc, CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat, CategoryTheory.ComposableArrows.homMk₅_app_five, AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, CategoryTheory.Limits.equalizerSubobject_arrow'_assoc, CategoryTheory.Abelian.SpectralObject.sc₂_X₃, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, SSet.Subcomplex.toSSetFunctor_map, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, TopologicalSpace.Opens.coe_inclusion', AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, TopologicalSpace.OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.StructureSheaf.const_self, CategoryTheory.Limits.hasColimitsOfShape_thinSkeleton, AlgebraicGeometry.Scheme.mem_basicOpen', CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp_assoc, CategoryTheory.Subobject.inf_le_left, CategoryTheory.Functor.WellOrderInductionData.map_succ, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₂, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, AlgebraicGeometry.Scheme.Opens.topIso_inv, Opens.pretopology_toGrothendieck, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff, CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE_val, AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE, CategoryTheory.Subobject.map_comp, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d, AlgebraicGeometry.Spec_presheaf, CategoryTheory.Functor.toOrderHom_coe, imageToKernel'_kernelSubobjectIso, CategoryTheory.Subobject.isPullback_aux, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, CategoryTheory.preservesFiniteColimits_liftToFinset, CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero, CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, CategoryTheory.Abelian.SpectralObject.δToCycles_πE, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial, Opens.mayerVietorisSquare_X₃, AlgebraicGeometry.Scheme.inv_app, CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom_assoc, CategoryTheory.ComposableArrows.scMap_τ₁, AlgebraicGeometry.Scheme.Hom.id_appTop, CategoryTheory.Abelian.SpectralObject.shortComplex_X₂, CondensedMod.isDiscrete_tfae, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, smoothSheafCommRing.ι_evalHom_apply, CategoryTheory.ThinSkeleton.map_map, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app, TopCat.Presheaf.germ_exist_of_isBasis, CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence, CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf_w, CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles, AlgebraicGeometry.image_morphismRestrict_preimage, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, conePt_mem_lowerBounds, CategoryTheory.Limits.kernelSubobject_arrow'_apply, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, HasCardinalLT.Set.functor_obj, AlgebraicGeometry.Proj.map_preimage_basicOpen, AlgebraicGeometry.Scheme.zeroLocus_mul, CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', TopologicalSpace.Opens.map_functor_eq', CategoryTheory.Subobject.factorThru_eq_zero, TopologicalSpace.OpenNhds.comp_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ, AlgebraicGeometry.SpecMap_preimage_basicOpen, ModuleCat.directLimitCocone_pt_carrier, CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero, CategoryTheory.isCofiltered_of_directed_ge_nonempty, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, smoothSheafCommRing.eval_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk, hasColimit_iff_hasLUB, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.Hom.image_le_image_of_le, CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map, CategoryTheory.Abelian.SpectralObject.δ_toCycles, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, CategoryTheory.TransfiniteCompositionOfShape.fac_assoc, AlgebraicGeometry.StructureSheaf.const_add, TopologicalSpace.Opens.map_obj, TopologicalSpace.Opens.comp_apply, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.Abelian.SpectralObject.δ_δ_assoc, CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles, OrderIso.equivalence_functor, AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le, CategoryTheory.ThinSkeleton.map_obj, TopologicalSpace.OpenNhds.val_apply, CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup, AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, CategoryTheory.ComposableArrows.homMk₃_app_three, TopCat.GlueData.ofOpenSubsets_toGlueData_U, CategoryTheory.Functor.WellOrderInductionData.surjective, TopologicalSpace.Opens.instIsContinuousCompGrothendieckTopology, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i, SSet.horn₃₂.desc.multicofork_π_one, IsOpenMap.pullbackObjIso_hom_app, TopologicalSpace.OpenNhds.inclusionMapIso_inv, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.structureSheafInType.mul_apply, TopCat.Presheaf.germ_stalkSpecializes_apply, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv, CategoryTheory.ComposableArrows.homMk₄_app_four, CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_H, CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app, AlgebraicGeometry.StructureSheaf.exists_const, CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_app, IsOpenMap.functorNhds_obj_coe, skyscraperPresheafCocone_pt, CategoryTheory.Subobject.top_arrow_isIso, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, TopCat.Sheaf.pushforward_map, CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_diagramFunctor, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.congr_app, TopologicalSpace.Opens.infLELeft_apply_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le', AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app, AlgebraicGeometry.locallyQuasiFinite_iff, AlgebraicGeometry.Scheme.preimage_comp, smoothSheaf.ι_evalHom_apply, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, IsOpenMap.pullbackObjIso_hom_naturality, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_one, TopCat.Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv_assoc, CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow, CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, TopCat.Presheaf.germ_res', CategoryTheory.Abelian.SpectralObject.cyclesMap_id, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj, AlgebraicGeometry.PresheafedSpace.Γ_obj_op, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_zero, TopologicalSpace.Opens.map_comp_obj_unop, CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero, CategoryTheory.Subobject.ofMkLE_arrow, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, TopCat.Sheaf.interUnionPullbackCone_fst, CategoryTheory.Subobject.map_top, AlgebraicGeometry.functionField_isScalarTower, imageToKernel_op, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, TopCat.Presheaf.stalkPushforward_germ_apply, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, factorThruImageSubobject_comp_imageToKernel, CategoryTheory.ThinSkeleton.fromThinSkeleton_map, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles, CategoryTheory.Limits.hasColimitsOfSize_thinSkeleton, CategoryTheory.Equivalence.toOrderIso_apply, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, CategoryTheory.Subobject.ofLE_arrow_assoc, AlgebraicGeometry.Scheme.exists_germ_injective, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_one, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, CategoryTheory.ComposableArrows.whiskerLeft_obj, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, HasCardinalLT.Set.cocone_pt, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isoBot, LightProfinite.proj_comp_transitionMapLE', CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape, CategoryTheory.Subobject.ofMkLE_comp_ofLEMk_assoc, TopCat.Presheaf.germ_res_apply, colimitCoconeOfIsLUB_cocone, AlgebraicGeometry.Scheme.Hom.preimage_top, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Proj.one_apply, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.isoSpec_hom, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_inv, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, CategoryTheory.Meq.pullback_refine, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, TopCat.Presheaf.germ_stalkPullbackInv_assoc, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, TopCat.Sheaf.exact_iff_stalkFunctor_map_exact, TopCat.GlueData.ofOpenSubsets_toGlueData_t, AlgebraicGeometry.Scheme.Hom.resLE_app_top, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_assoc, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app_assoc, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, SimpleGraph.componentComplFunctor_obj, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, coconePt_mem_upperBounds, AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_two, CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg, CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, Types.monoOverEquivalenceSet_inverse_map, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, CategoryTheory.Subobject.inf_comp_left, CategoryTheory.Abelian.SpectralObject.δ_δ, CategoryTheory.Abelian.SpectralObject.cyclesMap_i, IsOpenMap.functor_faithful, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, CategoryTheory.IsFiltered.exists_directed, AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncLT, AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, CategoryTheory.ShortComplex.mapToComposableArrows_app_1, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, CategoryTheory.Limits.kernelSubobject_arrow_assoc, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, AlgebraicGeometry.Scheme.zeroLocus_iUnion, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, AlgebraicGeometry.IsReduced.component_reduced, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, CategoryTheory.homOfLE_comp_eqToHom, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero, CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE_assoc, TopCat.Sheaf.id_app, TopologicalSpace.Opens.isOpenEmbedding_obj_top, AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, CategoryTheory.preservesFiniteLimits_liftToFinset, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, SimpleGraph.infinite_iff_in_eventualRange, CategoryTheory.Limits.kernelSubobjectMap_comp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, CategoryTheory.Triangulated.TStructure.spectralObject_ω₁, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, CategoryTheory.Abelian.SpectralObject.toCycles_descCycles, CategoryTheory.Limits.kernelSubobject_comp_mono_isIso, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀, AlgebraicGeometry.StructureSheaf.comap_const, AlgebraicGeometry.Scheme.Hom.appLE_map', AlgebraicGeometry.Scheme.Hom.image_iSup₂, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.zeroLocus_singleton, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.LocallyRingedSpace.component_nontrivial, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, CategoryTheory.Functor.ofSequence_map_homOfLE_succ, AlgebraicGeometry.Proj.sub_apply, AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover, AlgebraicGeometry.IsImmersion.instMorphismRestrict, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₁, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, AlgebraicGeometry.Scheme.Hom.resLE_map, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, CategoryTheory.Subobject.inf_arrow_factors_right, CategoryTheory.ComposableArrows.homMk₂_app_two, CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι_assoc, AlgebraicGeometry.Scheme.Hom.comp_app, ProfiniteGrp.toLimit_surjective, CategoryTheory.Limits.equalizerSubobject_arrow_comp, CategoryTheory.Limits.LimitPresentation.self_π, CategoryTheory.Subobject.prod_eq_inf, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le', CategoryTheory.TransfiniteCompositionOfShape.ici_F, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, TopologicalSpace.Opens.mapId_hom_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Proj.ι_comp_map, CategoryTheory.Abelian.SpectralObject.comp_hom, TopologicalSpace.Opens.mapComp_hom_app, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, lightDiagramToLightProfinite_obj, CategoryTheory.SubobjectRepresentableBy.homEquiv_eq, CategoryTheory.Subobject.ofLE_comp_ofLEMk_assoc, OrderHom.equivalenceFunctor_counitIso_inv_app_app, smoothSheaf.ι_evalHom_assoc, CategoryTheory.Abelian.SpectralObject.EToCycles_i_assoc, Profinite.isIso_indexCone_lift, CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.StructureSheaf.comap_apply, CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback, AlgebraicGeometry.Scheme.Hom.smooth_appLE, SSet.horn₃₁.desc.multicofork_pt, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, IsOpenMap.functorFullOfMono, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, CategoryTheory.ComposableArrows.homMk₅_app_zero, CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_f, CategoryTheory.ComposableArrows.precomp_obj, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.Scheme.comp_appLE, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, AlgebraicGeometry.isIso_fromTildeΓ_of_presentation, CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀', AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CategoryTheory.Triangulated.TStructure.ω₁_map, CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_two, CategoryTheory.ThinSkeleton.fromThinSkeleton_obj, CategoryTheory.OrthogonalReflection.iteration_map_succ, TopologicalSpace.Opens.map_id_obj', AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.Scheme.ofRestrict_appLE, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt, CategoryTheory.Subobject.factorThru_comp_arrow, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.Scheme.Hom.id_app, TopCat.Presheaf.comp_app, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_hom, AlgebraicGeometry.Scheme.Γ_obj, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂, SSet.Subcomplex.toSSetFunctor_obj, CategoryTheory.Abelian.SpectralObject.comp_hom_assoc, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.kerAdjunction_unit_app, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed, CategoryTheory.Abelian.SpectralObject.πE_ιE, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit, TopCat.Presheaf.germ_stalkSpecializes_assoc, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_obj_obj, CategoryTheory.Subobject.ofLEMk_comp, imageToKernel_comp_right, LightProfinite.lightToProfinite_map_proj_eq, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc, AlgebraicGeometry.Scheme.ΓSpecIso_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, TopologicalSpace.OpenNhds.map_obj, CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp, TopCat.Presheaf.stalkPushforward_germ_assoc, imageToKernel_comp_hom_inv_comp, AlgebraicGeometry.Scheme.opensRange_homOfLE, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, TopCat.Presheaf.pushforward_map_app, AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap, instFullFunctor, TopologicalSpace.OpenNhds.op_map_id_obj, AlgebraicGeometry.Scheme.isoSpec_hom_naturality_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, CategoryTheory.ComposableArrows.isoMkSucc_hom, AlgebraicGeometry.Scheme.germToFunctionField_injective, CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, ProfiniteGrp.denseRange_toLimit, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', CategoryTheory.homOfLE_op_comp_eqToHom_assoc, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom_assoc, CondensedMod.isDiscrete_iff_isDiscrete_forget, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃, CategoryTheory.Subobject.factorThru_mk_self, CategoryTheory.Subobject.ofLEMk_comp_ofMkLE, TopologicalSpace.Opens.map_homOfLE, imageToKernel_arrow_assoc, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_inv_app, CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom, AlgebraicGeometry.morphismRestrict_base, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat, CategoryTheory.ComposableArrows.isoMk₅_inv, CategoryTheory.ComposableArrows.homMkSucc_app_zero, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.zeroLocus_setMul, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀, CategoryTheory.ComposableArrows.exact_iff_δ₀, Alexandrov.principals_map, limitConeOfIsGLB_isLimit, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, CategoryTheory.homOfLE_refl, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, instHasTerminalOfOrderTop, CategoryTheory.ThinSkeleton.thin, TopologicalSpace.Opens.inclusion'_top_functor, CategoryTheory.ThinSkeleton.map₂_obj, TopCat.Presheaf.stalk_open_algebraMap, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Hom.app_surjective, CategoryTheory.Abelian.SpectralObject.isIso_fromOpcycles, CategoryTheory.Abelian.SpectralObject.zero₃, TopCat.GlueData.instIsIsoT, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq, CategoryTheory.ComposableArrows.homMk₄_app_three, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map, TopCat.Presheaf.pushforwardEq_hom_app, AlgebraicGeometry.affineLocally_iff_affineOpens_le, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, AlgebraicGeometry.RingedSpace.basicOpen_pow, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, TopCat.presheafToTop_obj, CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_ι, AlgebraicGeometry.HasRingHomProperty.iff_of_iSup_eq_top, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, AlgebraicGeometry.PresheafedSpace.Γ_map_op, CategoryTheory.Dial.comp_le_lemma, TopCat.Presheaf.pullbackObjObjOfImageOpen_hom_naturality, CategoryTheory.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.id_appTop, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_g, TopCat.Presheaf.germ_ext, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop_assoc, ModuleCat.cokernel_π_imageSubobject_ext, TopologicalSpace.Opens.map_functor_eq, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₁, TopCat.Sheaf.extend_hom_app, AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app_assoc, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, AlgebraicGeometry.Scheme.ker_toSpecΓ, TopCat.Presheaf.map_germ_eq_Γgerm, CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, PartialOrder.mem_nerve_degenerate_of_eq, CategoryTheory.Abelian.SpectralObject.exact₂', CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_map, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.isBasis_basicOpen, TopologicalSpace.Opens.map_id_obj, CategoryTheory.ComposableArrows.homMk₄_app_zero, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_larger_subobject, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt, AlgebraicGeometry.Scheme.Hom.mem_preimage, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, PartialOrder.mem_nerve_nonDegenerate_iff_injective, CategoryTheory.Adjunction.gc, CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero, AlgebraicGeometry.Scheme.Γevaluation_naturality_apply, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p, AlgebraicGeometry.locallyOfFiniteType_iff, AlgebraicGeometry.SheafedSpace.comp_c_app, CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map, AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, TopCat.Presheaf.SheafConditionEqualizerProducts.w, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, CategoryTheory.Subobject.pullback_id, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, CategoryTheory.Abelian.SpectralObject.p_opcyclesToE, CategoryTheory.Triangulated.SpectralObject.triangle_obj₂, CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_H, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, TopCat.Presheaf.isSheaf_iff_isSheaf_comp, CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ι_app, CategoryTheory.Subobject.pullback_obj, AlgebraicGeometry.isIntegral_appTop_of_universallyClosed, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.Scheme.zeroLocus_def, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app, AlgebraicGeometry.ΓSpec.adjunction_counit_app, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux, CompleteLattice.MulticoequalizerDiagram.multispanIndex_right, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.tilde.isoTop_hom, instHasInitialOfOrderBot, AlgebraicGeometry.Scheme.restrict_presheaf_obj, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux, ModuleCat.Tilde.toOpen_res, colimitCoconeOfIsLUB_isColimit, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_ι_app, CompleteLattice.MulticoequalizerDiagram.multispanIndex_fst, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_map, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop, CategoryTheory.ComposableArrows.map'_comp, CategoryTheory.ComposableArrows.IsComplex.zero_assoc, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, InfiniteGalois.mulEquivToLimit_symm_continuous, SSet.horn₃₁.desc.multicofork_π_two_assoc, IsOpenMap.pullbackIso_inv_app_app, CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles_assoc, AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Spec.map_appLE, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map, AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE, smoothSheafCommRing.ι_evalHom, AlgebraicGeometry.Γ_restrict_isLocalization, CategoryTheory.Abelian.SpectralObject.isIso_toCycles, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum, CategoryTheory.ComposableArrows.isoMk₄_hom, CategoryTheory.Subobject.map_pullback, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, AlgebraicGeometry.Scheme.Hom.app_eq, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, AlgebraicGeometry.RingedSpace.res_zero, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, PrincipalSeg.cocone_ι_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, CategoryTheory.Pairwise.cocone_pt, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, SSet.horn₃₁.desc.multicofork_π_zero_assoc, CategoryTheory.Abelian.SpectralObject.shortComplexMap_id, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom, ModuleCat.directLimitIsColimit_desc, CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.ΓSpecIso_obj_hom, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot, TopologicalSpace.Opens.map_comp_map, CategoryTheory.Subobject.inf_eq_map_pullback', CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le, CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_naturality_assoc, coconeOfUpperBound_pt, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, ModuleCat.directLimitCocone_pt_isAddCommGroup, AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset, CategoryTheory.Functor.ofOpSequence_obj, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, CategoryTheory.instIsCardinalFilteredToTypeOrd, AlgebraicGeometry.Scheme.Modules.restrict_map, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, imageToKernel_epi_comp, AlgebraicGeometry.injective_germ_basicOpen, TopologicalSpace.Opens.functor_obj_map_obj, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.WeaklyEtale.instMorphismRestrict, CategoryTheory.Subobject.instMonoOfLE, AlgebraicGeometry.HasRingHomProperty.iff_appLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_map_assoc, AlgebraicGeometry.Scheme.Hom.image_mono, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, CategoryTheory.Subobject.mapIsoToOrderIso_apply, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit, CategoryTheory.Adhesive.instHasBinaryCoproductsSubobject, TopCat.Presheaf.app_surjective_of_injective_of_locally_surjective, TopologicalSpace.Opens.map_comp_obj', CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃, AlgebraicGeometry.StructureSheaf.const_mul_cancel, ProfiniteGrp.cone_pt, CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow, TopologicalSpace.Opens.mapMapIso_functor, CategoryTheory.Limits.ColimitPresentation.self_diag, CategoryTheory.Subobject.factorThru_arrow_assoc, CategoryTheory.Functor.monotone, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, CategoryTheory.Triangulated.TStructure.eTruncGEπ_top, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, AlgebraicGeometry.HasAffineProperty.restrict, CategoryTheory.ComposableArrows.δ₀Functor_obj_map, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₂, CategoryTheory.Limits.pullback_factors_iff, CategoryTheory.Subobject.arrow_mono, CategoryTheory.Subobject.isIso_top_arrow, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc, limitConeOfIsGLB_cone, AlgebraicGeometry.Scheme.Γevaluation_naturality_assoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoAppIncl, AlgebraicGeometry.Scheme.kerAdjunction_counit_app, AlgebraicGeometry.opensDiagramι_app, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_one, TopologicalSpace.Opens.mapIso_inv_app, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, CategoryTheory.ComposableArrows.isoMkSucc_inv, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Limits.CompleteLattice.hasLimits_of_completeLattice, CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ_assoc, AlgebraicGeometry.Scheme.component_nontrivial, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, CategoryTheory.TransfiniteCompositionOfShape.map_isoBot, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, CategoryTheory.Subobject.hasLimitsOfShape, TopologicalSpace.Opens.coe_overEquivalence_functor_obj, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.Scheme.basicOpen_pow, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₂, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, AlgebraicGeometry.HasRingHomProperty.appLE, AlgebraicGeometry.Scheme.Hom.ker_apply, CategoryTheory.Abelian.SpectralObject.sc₂_g, CategoryTheory.Subobject.factors_comp_arrow, TopCat.Sheaf.existsUnique_gluing, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, CochainComplex.mappingConeCompTriangle_mor₃_naturality, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ_assoc, CategoryTheory.Limits.imageSubobjectIso_comp_image_map, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj, hasLimit_iff_hasGLB, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, TopologicalSpace.OpenNhds.id_apply, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor, CategoryTheory.Subobject.factors_self, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, CategoryTheory.TransfiniteCompositionOfShape.fac, CategoryTheory.Limits.imageSubobject_zero_arrow, CategoryTheory.Pairwise.diagram_map, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id, coneOfLowerBound_pt, subsingleton_hom, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_assoc, CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles, AlgebraicGeometry.Scheme.evaluation_eq_zero_iff_notMem_basicOpen, CategoryTheory.Subfunctor.equivalenceMonoOver_inverse_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, finGaloisGroupMap.map_id, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, InfiniteGalois.proj_adjoin_singleton_val, TopCat.Presheaf.stalk_mono_of_mono, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.subobject_simple_iff_isAtom, CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow, TopCat.Presheaf.map_germ_eq_Γgerm_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, TopologicalSpace.Opens.op_map_id_obj, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, TopCat.Presheaf.app_surjective_of_stalkFunctor_map_bijective, CategoryTheory.Abelian.SpectralObject.δToCycles_πE_assoc, AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ, CategoryTheory.Subobject.map_bot, AlgebraicGeometry.Scheme.zeroLocus_radical, CategoryTheory.TransfiniteCompositionOfShape.map_isColimit, TopCat.Sheaf.interUnionPullbackConeLift_right, Opens.instIsThinPointOpensGrothendieckTopology, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, LightProfinite.Extend.functor_map, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.exists_map_preimage_eq_map_preimage, CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift, CategoryTheory.Abelian.SpectralObject.sc₁_X₁, CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.Scheme.Hom.map_appLE_assoc, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, TopologicalSpace.Opens.mapMapIso_unitIso, TopologicalSpace.OpenNhds.map_id_obj_unop, AlgebraicGeometry.StructureSheaf.const_one, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app, CategoryTheory.Subobject.factorThru_add_sub_factorThru_right, AlgebraicGeometry.Scheme.Opens.ι_appIso, CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, CompleteLattice.MulticoequalizerDiagram.multispanIndex_left, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, CategoryTheory.ComposableArrows.sc'MapIso_hom, AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f, TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, CategoryTheory.toThinSkeleton_map, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, AlgebraicGeometry.Scheme.basicOpen_add_le, AlgebraicGeometry.Scheme.Hom.comp_app_assoc, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ_assoc, AlgebraicGeometry.Scheme.comp_app, Opens.isConservativeFamilyOfPoints_pointsGrothendieckTopology, CategoryTheory.Abelian.SpectralObject.zero₂, TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top, AlgebraicGeometry.Scheme.zeroLocus_map, AlgebraicGeometry.Scheme.Hom.finite_app, TopCat.Presheaf.stalk_hom_ext_iff, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, HomotopyCategory.composableArrowsFunctor_obj, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app, AlgebraicGeometry.Scheme.evaluation_naturality, Alexandrov.principals_obj, AlgebraicGeometry.ΓSpec.left_triangle, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_map_hom, AlgebraicGeometry.AffineSpace.comp_homOfVector, AlgebraicGeometry.smooth_iff, CategoryTheory.ComposableArrows.scMapIso_inv, AlgebraicGeometry.Scheme.Hom.appIso_hom', TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, AlgebraicGeometry.Scheme.zeroLocus_inf, CategoryTheory.SmallObject.coconeOfLE_pt, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, AlgebraicGeometry.Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.StructureSheaf.smul_const, TopCat.Presheaf.pushforward_obj_obj, CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app_assoc, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, CategoryTheory.ComposableArrows.mk₁_obj, CategoryTheory.ComposableArrows.map'_inv_eq_inv_map', IsOpenMap.pullbackObjIso_inv_app, AlgebraicGeometry.Scheme.Hom.resLE_congr, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.AffineSpace.hom_ext_iff, CategoryTheory.Subobject.isoOfEq_hom, SSet.stdSimplex.isoNerve_hom_app_apply, CategoryTheory.ComposableArrows.homMk₅_app_two, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, TopCat.Presheaf.app_bijective_of_stalkFunctor_map_bijective, instHasColimitsOfShape, CategoryTheory.SmallObject.ιFunctorObj_eq, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, CategoryTheory.ComposableArrows.whiskerLeft_map, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, CategoryTheory.Subobject.lower_comm, CategoryTheory.ComposableArrows.Exact.isIso_map', CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc, imageToKernel_arrow, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, Opens.mayerVietorisSquare_X₂, Monotone.final_functor_iff, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.Hom.app_invApp', TopCat.GlueData.MkCore.t_inv, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app, AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top, AlgebraicGeometry.Scheme.image_basicOpen, CategoryTheory.Subobject.inf_isPullback, AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit, AlgebraicGeometry.tilde.isIso_toOpen_top, PartialOrder.mem_range_nerve_σ_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, TopCat.Presheaf.SubmonoidPresheaf.map, CategoryTheory.isCofilteredOrEmpty_of_semilatticeInf, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles, CategoryTheory.Limits.LimitPresentation.self_diag, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_assoc, AlgebraicGeometry.HasRingHomProperty.appTop, AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, CategoryTheory.Subobject.mk_arrow, TopCat.Sheaf.existsUnique_gluing', AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₂, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot, CategoryTheory.ThinSkeleton.thinSkeleton_isSkeleton, Topology.IsUpperSet.isSheaf_of_isRightKanExtension, CategoryTheory.Limits.imageSubobject_arrow_comp_apply, AlgebraicGeometry.IsIntegral.component_integral, AlgebraicGeometry.morphismRestrict_comp, CategoryTheory.Abelian.SpectralObject.instEpiToCycles, CategoryTheory.Subobject.isoOfEqMk_inv, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, CategoryTheory.ComposableArrows.mapFunctorArrows_app, AlgebraicGeometry.StructureSheaf.const_zero, TopologicalSpace.Opens.coe_id, CategoryTheory.ShortComplex.mapToComposableArrows_comp, CategoryTheory.Subfunctor.equivalenceMonoOver_functor_obj, AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc, AlgebraicGeometry.IsProper.instMorphismRestrict, TopCat.presheafToTypes_map, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₁, AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, CategoryTheory.Functor.mapComposableArrows_obj_map, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles_assoc, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_ι, CategoryTheory.Abelian.SpectralObject.exact₃', AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, TopologicalSpace.Opens.set_range_inclusion', CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, CategoryTheory.Limits.kernelSubobject_arrow_comp_apply, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor, CategoryTheory.Pairwise.cocone_ι_app, CategoryTheory.ComposableArrows.isoMk₂_inv, TopCat.Sheaf.comp_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, smoothSheafCommRing.ι_forgetStalk_inv_apply, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, CategoryTheory.isEventuallyConstant_of_isArtinianObject, AlgebraicGeometry.SheafedSpace.Γ_map, Opens.coe_mayerVietorisSquare_X₁, CategoryTheory.Subobject.isoOfMkEq_inv, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, CategoryTheory.Subobject.underlyingIso_arrow, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_top, AlgebraicGeometry.germ_stalkClosedPointIso_hom, TopCat.Presheaf.isLocallySurjective_iff, TopCat.Sheaf.IsFlasque.epi_of_shortExact, AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv, AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop, CategoryTheory.Subobject.ofLE_comp_ofLE_assoc, CategoryTheory.Subobject.instMonoOfLEMk, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π_assoc, CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap, CategoryTheory.Triangulated.TStructure.ω₁_obj, CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂, AlgebraicGeometry.Proj.awayToSection_comp_appLE, TopologicalSpace.Opens.mapMapIso_inverse, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, TopCat.Presheaf.Pushforward.comp_inv_app, AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor, TopCat.Presheaf.covering_presieve_eq_self, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality, AlgebraicGeometry.Scheme.evaluation_naturality_apply, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.toSpecΓ_appTop, CategoryTheory.Dial.Hom.le, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_app, PrincipalSeg.cocone_pt, CategoryTheory.Triangulated.SpectralObject.triangle_mor₂, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc, imageToKernel_epi_of_zero_of_mono, smoothSheaf.obj_eq, TopologicalSpace.Opens.mapId_inv_app, CategoryTheory.ShortComplex.mapToComposableArrows_app_2, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map_f', CategoryTheory.Abelian.SpectralObject.iCycles_δ, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, CategoryTheory.ComposableArrows.naturality', AlgebraicGeometry.Scheme.Hom.comp_appIso, AlgebraicGeometry.Scheme.basicOpen_one, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.Scheme.Modules.Hom.id_app, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, TopologicalSpace.Opens.inclusion'_map_eq_top, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc, CategoryTheory.Abelian.SpectralObject.Hom.comm, CategoryTheory.Subobject.instIsEquivalenceMonoOverRepresentative, TopCat.Sheaf.pushforward_obj_val, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq, OrderIso.equivalence_counitIso, CategoryTheory.TransfiniteCompositionOfShape.iic_F, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_f, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, TopCat.Sheaf.sections_exact_of_left_exact, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_hom_app, CategoryTheory.Limits.CompleteLattice.pushout_eq_sup, CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, CategoryTheory.ComposableArrows.sc'Map_τ₁, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, CategoryTheory.ComposableArrows.isoMk_inv, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, TopCat.Presheaf.stalkFunctor_map_germ_apply, TopCat.Presheaf.germ_res_apply', CategoryTheory.Subobject.ofMkLE_comp_ofLEMk, TopCat.Opens.coverDense_inducedFunctor, CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₂, imageToKernel_comp_left, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id, AlgebraicGeometry.Scheme.Opens.ι_appTop, CategoryTheory.SmallObject.SuccStruct.arrowι_def, AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.map_mem_image_iff, CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, TopologicalSpace.Opens.overEquivalence_counitIso_inv_app, ModuleCat.directLimitDiagram_obj_isAddCommGroup, CategoryTheory.isCofiltered_of_semilatticeInf_nonempty, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_obj, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, CategoryTheory.SmallObject.restrictionLE_map, TopologicalSpace.Opens.adjunction_counit_map_functor, CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc, CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Proj.zero_apply, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles_assoc, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans_assoc, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, CategoryTheory.ComposableArrows.mk₀_obj, OrderHom.equivalenceFunctor_functor_obj_obj, AlgebraicGeometry.exists_affineOpens_le_appLE_of_appLE, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, AlgebraicGeometry.affinePreimage, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat, coconeOfUpperBound_ι_app, AlgebraicGeometry.Scheme.isoSpec_inv_naturality, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, Types.monoOverEquivalenceSet_functor_map, CategoryTheory.Subobject.eq_of_comp_arrow_eq_iff, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc, TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left, AlgebraicGeometry.StructureSheaf.const_algebraMap, CategoryTheory.Regular.instIsRegularEpiFrobeniusMorphism, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_assoc, CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one, AlgebraicGeometry.Scheme.Hom.id_appIso, CategoryTheory.GrothendieckTopology.diagram_map, CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT, smoothSheafCommRing.ι_forgetStalk_inv_assoc, skyscraperPresheafCocone_ι_app, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, CategoryTheory.Triangulated.SpectralObject.id_hom, CategoryTheory.ComposableArrows.homMkSucc_app_succ, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_obj, CategoryTheory.Limits.imageSubobjectMap_arrow, AlgebraicGeometry.PresheafedSpace.map_id_c_app, compatiblePreserving_opens_map, TopCat.Presheaf.germ_exist, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, AlgebraicGeometry.Scheme.comp_appTop_assoc, CategoryTheory.Limits.imageSubobjectMap_arrow_assoc, CategoryTheory.Abelian.SpectralObject.sc₂_X₁, CategoryTheory.GrothendieckTopology.diagramPullback_app, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, AlgebraicGeometry.Scheme.local_affine, TopCat.Presheaf.germ_res, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc, TopologicalSpace.Opens.adjunction_counit_app_self, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, TopologicalSpace.Opens.mem_map, AlgebraicGeometry.Scheme.Hom.etale_appLE, PartialOrder.isIso_iff_eq, CategoryTheory.ComposableArrows.mk₁_map, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, IsOpenMap.coverPreserving, AlgebraicGeometry.Scheme.isoSpec_Spec, CategoryTheory.Limits.kernelSubobject_arrow, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_two, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.Scheme.Hom.appLE_congr, CategoryTheory.Limits.Types.isPushout_of_bicartSq, TopCat.Presheaf.Pushforward.id_hom_app, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, TopCat.Presheaf.pullback_obj_obj_ext_iff, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, TopCat.Opens.coverDense_iff_isBasis, CategoryTheory.Subobject.ofLE_refl, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_e, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, AlgebraicGeometry.Scheme.Hom.preimage_sup, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, CategoryTheory.eqToHom_comp_homOfLE, CategoryTheory.ComposableArrows.isComplex₂_iff, AlgebraicGeometry.IsClosedImmersion.hasAffineProperty, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, TopCat.Presheaf.app_injective_of_stalkFunctor_map_injective, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, CategoryTheory.isCardinalFiltered_preorder, CategoryTheory.Abelian.SpectralObject.zero₁, CategoryTheory.Subobject.factorThru_self, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk_assoc, LightProfinite.Extend.functorOp_map, instHasBinaryCoproducts, TopCat.Sheaf.interUnionPullbackConeLift_left, AlgebraicTopology.NormalizedMooreComplex.d_squared, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE, TopCat.subpresheafToTypes_map_coe, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, AlgebraicGeometry.Scheme.Hom.image_iSup, CategoryTheory.ComposableArrows.δlastFunctor_obj_obj, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, Alexandrov.lowerCone_π_app, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, TopologicalSpace.Opens.map_comp_eq, imageSubobjectIso_imageToKernel', CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, Types.monoOverEquivalenceSet_functor_obj, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, CategoryTheory.Limits.imageSubobject_arrow, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.SheafedSpace.Γ_obj_op, CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.kerFunctor_map, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF, instHasLimitsOfShape, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity, CategoryTheory.Limits.CompleteLattice.pullback_eq_inf, CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, TopCat.Presheaf.pushforward_map_app', AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, CategoryTheory.Abelian.SpectralObject.δ_naturality, CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom_assoc, CategoryTheory.Subobject.imageFactorisation_F_I, CategoryTheory.Abelian.SpectralObject.sc₃_X₁, AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, AlgebraicGeometry.Scheme.homOfLE_appLE, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc, CategoryTheory.Subobject.inf_map, TopCat.Presheaf.pushforward_obj_map, CategoryTheory.ComposableArrows.scMapIso_hom, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot, AlgebraicGeometry.Scheme.inv_appTop, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj, AlgebraicGeometry.isLocalization_away_of_isAffine, AlgebraicGeometry.Scheme.Hom.isIso_app, CategoryTheory.SemilatticeInf.tensorUnit, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Scheme.basicOpen_appLE, TopologicalSpace.Opens.map_iSup, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_refl, CategoryTheory.Limits.CompleteLattice.hasColimits_of_completeLattice, CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_π, ProfiniteGrp.cone_π_app, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_three, CategoryTheory.Triangulated.SpectralObject.distinguished', AlgebraicGeometry.structureSheafInType.add_apply, instMonoImageToKernel, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, CategoryTheory.Triangulated.SpectralObject.triangle_mor₁, TopCat.Presheaf.stalkPushforward_germ, CategoryTheory.ComposableArrows.isoMk₃_hom, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, CategoryTheory.ThinSkeleton.map_id_eq, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, TopCat.Presheaf.germ_stalkPullbackHom_assoc, TopCat.subsheafToTypes_obj, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, AlgebraicGeometry.LocallyRingedSpace.Γ_map, CategoryTheory.Subobject.factorThru_ofLE, AlgebraicGeometry.Flat.flat_of_affine_subset, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, CategoryTheory.ComposableArrows.scMap_τ₃, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_zero, CategoryTheory.ComposableArrows.δlastFunctor_map_app, CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.of_isStableUnderColimitsOfShape.mem_map_bot_le, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape, TopCat.GlueData.MkCore.t_id, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_K, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, isLUB_of_isColimit, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles_assoc, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_incl, Opens.instHasEnoughPointsOpensGrothendieckTopology, IsOpenMap.functorNhds_map, CategoryTheory.Limits.equalizerSubobject_arrow, CategoryTheory.ThinSkeleton.map₂_map, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.PresheafedSpace.Γ_obj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, CategoryTheory.Subobject.instMonoOfMkLE, CategoryTheory.Abelian.SpectralObject.id_hom, CategoryTheory.Limits.imageSubobject_arrow_comp_assoc, Topology.IsOpenEmbedding.functor_obj_injective, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, HomotopyCategory.composableArrowsFunctor_map, CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow, CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence, CategoryTheory.Triangulated.TStructure.isLE_eTruncLT_obj_obj, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map, AlgebraicGeometry.IsLocalAtTarget.restrict, Topology.IsInducing.map_functorObj, TopCat.Presheaf.germ_stalkPullbackInv, CategoryTheory.ThinSkeleton.skeletal, CategoryTheory.ComposableArrows.sc'Map_τ₃, CategoryTheory.nerve.δ_obj, CondensedSet.isDiscrete_tfae, SSet.horn₃₂.desc.multicofork_π_zero_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_incl, TopologicalSpace.Opens.leSupr_apply_mk, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, CategoryTheory.Subobject.le_inf, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀', CategoryTheory.Subobject.bot_arrow, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicTopology.NormalizedMooreComplex.map_f, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃, CategoryTheory.orderDualEquivalence_counitIso, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, CategoryTheory.Subobject.lowerEquivalence_counitIso, CompleteLattice.MulticoequalizerDiagram.multispanIndex_snd, CategoryTheory.Abelian.SpectralObject.map_comp, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, CategoryTheory.Abelian.SpectralObject.sc₂_X₂, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_bounded, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_obj, AlgebraicGeometry.Scheme.toOpen_eq, OrderHom.equivFunctor_apply, CategoryTheory.ComposableArrows.homMk₄_app_one, TopCat.Presheaf.map_restrict, AlgebraicGeometry.Scheme.Modules.restrict_obj, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac, CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ, CategoryTheory.orderDualEquivalence_functor_obj, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, CategoryTheory.coherentTopology.epi_π_app_zero_of_epi, CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv, OrderHom.equivalenceFunctor_counitIso_hom_app_app, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, CategoryTheory.ComposableArrows.homMk₅_app_three, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality, CategoryTheory.Abelian.SpectralObject.p_descOpcycles, AlgebraicGeometry.Scheme.directedAffineCover_trans, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top, TopologicalSpace.Opens.functor_map_eq_inf, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁, AlgebraicGeometry.StructureSheaf.comapₗ_const, CategoryTheory.SmallObject.πFunctorObj_eq, TopCat.Presheaf.restrictOpenCommRingCat_apply, AlgebraicGeometry.Scheme.Hom.isIntegral_app, HasCardinalLT.Set.cocone_ι_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq, CategoryTheory.ComposableArrows.homMk₃_app_two, CategoryTheory.Limits.pullback_factors, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, CategoryTheory.Limits.IsFiltered.sequentialFunctor_final, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, AlgebraicGeometry.StructureSheaf.res_apply, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.Scheme.Modules.Hom.add_app, CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp, CategoryTheory.Subobject.ofLE_comp_ofLEMk, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, InfiniteGalois.toAlgEquivAux_eq_liftNormal, TopologicalSpace.OpenNhds.isOpenEmbedding, CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app_assoc, OrderHom.equivalenceFunctor_unitIso_hom_app, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.exists_map_preimage_le_map_preimage, CategoryTheory.Subobject.factorThru_add_sub_factorThru_left, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf, CategoryTheory.Subobject.inf_def, AlgebraicGeometry.Scheme.Hom.map_appLE', CategoryTheory.Subobject.isoOfMkEq_hom, AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.Hom.inv_appTop, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, CategoryTheory.Subobject.skeletal, CategoryTheory.Subobject.pullback_map_self, CategoryTheory.Limits.imageSubobject_arrow'_assoc, CategoryTheory.Subobject.factorThru_arrow, localCohomology.ideal_powers_initial, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.Flat.flat_appLE, AlgebraicGeometry.isIntegralHom_iff, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id, TopCat.GlueData.ofOpenSubsets_toGlueData_V, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app, CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀, CategoryTheory.Subobject.inf_arrow_factors_left, AlgebraicGeometry.RingedSpace.basicOpen_res_eq, AlgebraicGeometry.Spec_zeroLocus, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE, AlgebraicGeometry.Scheme.basicOpen_mul, CategoryTheory.homOfLE_comp, AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality, CategoryTheory.Subobject.isoOfEq_inv, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, CategoryTheory.ShortComplex.toComposableArrows_map, CategoryTheory.Abelian.SpectralObject.Hom.comm_assoc, AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, CategoryTheory.ComposableArrows.isoMk₅_hom, AlgebraicGeometry.exists_app_map_eq_map_of_isLimit, CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, CategoryTheory.NatTrans.ofSequence_app, TopCat.GlueData.ofOpenSubsets_toGlueData_f, CategoryTheory.Subobject.factorThru_add, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_two, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, ProfiniteGrp.toLimit_injective, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit, CategoryTheory.Abelian.SpectralObject.sc₁_X₃, CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map, CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc, CategoryTheory.Regular.frobeniusMorphism_isPullback, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, CategoryTheory.Subobject.lowerEquivalence_unitIso, CategoryTheory.ComposableArrows.isoMk₀_inv_app, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_two, TopCat.Presheaf.isSheaf_iff_isSheaf_comp', AlgebraicGeometry.StructureSheaf.algebraMap_germ, imageToKernel_arrow_apply, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, TopologicalSpace.OpenNhds.inclusion_obj, SSet.horn₃₁.desc.multicofork_π_three_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right, AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow, CategoryTheory.GrothendieckTopology.diagramFunctor_map, CategoryTheory.Limits.CompleteLattice.prod_eq_inf, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_one, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, HasCardinalLT.Set.functor_map_coe, CategoryTheory.Triangulated.SpectralObject.comp_hom, AlgebraicGeometry.basicOpen_eq_of_affine', CategoryTheory.Subfunctor.equivalenceMonoOver_unitIso, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functor, AlgebraicGeometry.Scheme.Hom.coe_image, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AlgebraicGeometry.Scheme.Hom.coe_preimage, CategoryTheory.SubobjectRepresentableBy.isPullback, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id, CategoryTheory.ComposableArrows.homMk₂_app_zero, ModuleCat.directLimitDiagram_obj_carrier, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq, CategoryTheory.ComposableArrows.isoMk_hom, SSet.horn₃₁.desc.multicofork_π_zero, CategoryTheory.ComposableArrows.scMap_τ₂, CategoryTheory.orderDualEquivalence_functor_map, CategoryTheory.Abelian.SpectralObject.p_descOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀', AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, CategoryTheory.ComposableArrows.isIso_iff₀, smoothSheafCommRing.ι_forgetStalk_hom_apply, OrderIso.equivalence_inverse, TopologicalSpace.OpenNhds.map_id_obj', TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.StructureSheaf.const_mul_cancel', AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.Limits.equalizerSubobject_arrow', AlgebraicGeometry.Proj.awayι_preimage_basicOpen, Topology.IsInducing.functorNhds_obj_coe, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, AlgebraicGeometry.IsFinite.finite_app, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, CategoryTheory.Subobject.underlying_arrow_assoc, TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType, TopologicalSpace.Opens.coe_overEquivalence_inverse_obj_left, Topology.IsInducing.functor_obj, AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, TopCat.Presheaf.IsFlasque.epi, OrderHom.equivalenceFunctor_inverse_obj, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, AlgebraicGeometry.Proj.awayMap_awayToSection, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ', AlgebraicGeometry.Scheme.Hom.map_resLE, AlgebraicGeometry.finite_appTop_of_universallyClosed, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, CategoryTheory.homOfLE_op_comp_eqToHom, CategoryTheory.Subobject.pullback_obj_mk, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map, CategoryTheory.GrothendieckTopology.diagramFunctor_obj, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F, AlgebraicGeometry.IsIntegralHom.integral_app, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Subobject.ofLE_comp_ofLE, instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor, Monotone.functor_obj, AlgebraicGeometry.Scheme.Hom.resLE_preimage, CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, CategoryTheory.Subobject.ofMkLE_comp_ofLE, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, CategoryTheory.Limits.kernelSubobject_arrow'_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, imageToKernel_zero_right, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, AlgebraicGeometry.specTargetImageFactorization_app_injective, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj, preordToCat_obj, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, CategoryTheory.Presheaf.isLocallySurjective_toPlus, CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, CategoryTheory.Subobject.isPullback, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.Abelian.SpectralObject.instEpiPOpcycles, TopologicalSpace.Opens.op_map_comp_obj, AlgebraicGeometry.SheafedSpace.id_c_app, TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, AlgebraicGeometry.isPullback_morphismRestrict, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq, CategoryTheory.Limits.equalizerSubobject_arrow_assoc, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, AlgebraicGeometry.Scheme.Hom.appIso_hom, CategoryTheory.Subobject.isIso_arrow_iff_eq_top, CategoryTheory.Triangulated.TStructure.ω₁δ_app, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CategoryTheory.ComposableArrows.isoMk₂_hom, CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc, preordToCat_map, CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm, coneOfLowerBound_π_app, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat, CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, CategoryTheory.ComposableArrows.isoMk₃_inv, ModuleCat.directLimitCocone_ι_app, AlgebraicGeometry.tilde.toOpen_res, Alexandrov.projSup_obj, AlgebraicGeometry.tilde.toOpen_res_assoc, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_H, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one, CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles_assoc, AlgebraicGeometry.Scheme.emptyTo_c_app, TopCat.presheafToType_obj, SSet.horn₃₂.desc.multicofork_π_three, CategoryTheory.exists_simple_subobject, CategoryTheory.GrothendieckTopology.diagramNatTrans_app, AlgebraicGeometry.Scheme.Hom.map_resLE_assoc, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_one, HomotopyCategory.spectralObjectMappingCone_ω₁, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app, AlgebraicGeometry.Scheme.Hom.image_le_opensRange, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app, AlgebraicGeometry.AffineSpace.reindex_appTop_coord, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, AlgebraicGeometry.smoothOfRelativeDimension_iff, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, HasCardinalLT.Set.instIsCardinalFiltered, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE, CategoryTheory.Subobject.underlyingIso_inv_top_arrow, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, CategoryTheory.isFilteredOrEmpty_of_directed_le, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, AlgebraicGeometry.Scheme.empty_presheaf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map, TopCat.Presheaf.germ_res'_assoc, AlgebraicGeometry.Scheme.Opens.ι_app_self, LightCondensed.epi_π_app_zero_of_epi, TopologicalSpace.Opens.mapComp_inv_app, CategoryTheory.Functor.WellOrderInductionData.Extension.compatibility, AlgebraicGeometry.ΓSpec.toSpecΓ_of, AlgebraicGeometry.Scheme.zeroLocus_span, CategoryTheory.Functor.mapComposableArrows_obj_obj, AlgebraicGeometry.StructureSheaf.toOpen_germ, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.Scheme.Hom.image_injective, CategoryTheory.Subobject.inf_le_right, AlgebraicGeometry.exists_appTop_π_eq_of_isLimit, AlgebraicGeometry.Proj.stalkIso'_germ, TopCat.Presheaf.isGluing_iff_pairwise, Alexandrov.lowerCone_pt, SimplexCategory.toCat_obj, CategoryTheory.Subobject.underlyingIso_top_hom, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE, AlgebraicGeometry.SheafedSpace.Γ_obj, CategoryTheory.SmallObject.SuccStruct.iterationCocone_pt, CategoryTheory.ShortComplex.toComposableArrows_obj, AlgebraicGeometry.Scheme.restrict_presheaf_map, CategoryTheory.Abelian.SpectralObject.opcyclesMap_id, CategoryTheory.Subobject.ofMkLE_comp_ofLE_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.formallyUnramified_iff, CategoryTheory.Subfunctor.range_subobjectMk_ι, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right, TopCat.Sheaf.eq_app_of_locally_eq, CategoryTheory.GrothendieckTopology.preservesLimits_diagramFunctor, CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc, CategoryTheory.Abelian.SpectralObject.liftCycles_i, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone, CategoryTheory.ComposableArrows.homMk₃_app_one, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc, CategoryTheory.Abelian.SpectralObject.EToCycles_i, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.isCardinalFiltered, CategoryTheory.Abelian.SpectralObject.zero₃_assoc, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀', Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover, Types.monoOverEquivalenceSet_inverse_obj, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, SimpleGraph.componentComplFunctor_finite, CategoryTheory.isFiltered_of_semilatticeSup_nonempty, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, CategoryTheory.ComposableArrows.δ₀Functor_obj_obj, Fin.castSuccFunctor_obj, CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingPropertyFixedBot_ι_app_bot, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj, AlgebraicGeometry.Scheme.basicOpen_res, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, CategoryTheory.Subobject.arrow_congr, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app_assoc, TopologicalSpace.Opens.mapIso_hom_app, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, smoothSheaf.ι_evalHom, CategoryTheory.toThinSkeleton_obj, AlgebraicGeometry.Smooth.exists_isStandardSmooth, AlgebraicGeometry.Scheme.comp_appTop, smoothSheafCommRing.ι_evalHom_assoc, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, TopCat.Presheaf.Pushforward.comp_hom_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpen, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app, AlgebraicGeometry.IsClosedImmersion.isAffine_surjective_of_isAffine, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, CategoryTheory.Subobject.inf_comp_left_assoc, CategoryTheory.ComposableArrows.map'_self, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, AlgebraicGeometry.isIso_pushoutSection_iff, AlgebraicGeometry.Scheme.fromSpecStalk_app, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.Smooth.smooth_appLE, TopCat.GlueData.MkCore.t_inter, AlgebraicGeometry.StructureSheaf.res_const, CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_X₁, CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isColimit, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine, CategoryTheory.Subobject.pullback_top, CategoryTheory.Abelian.SpectralObject.shortComplex_X₁, CompleteLattice.MulticoequalizerDiagram.multicofork_pt, AlgebraicGeometry.isField_of_universallyClosed, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac', AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.exists_of_res_zero_of_qcqs, Opens.mayerVietorisSquare'_toSquare, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, CategoryTheory.Functor.WellOrderInductionData.map_lift, CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_obj, smoothSheafCommRing.ι_forgetStalk_hom, CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀', CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.aux, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen, InfiniteGalois.mk_toAlgEquivAux, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, CategoryTheory.ComposableArrows.homMk₅_app_one, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, CategoryTheory.StructuredArrow.projectSubobject_factors, Opens.coe_mayerVietorisSquare_X₄, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₁, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk, CategoryTheory.Subobject.pullback_comp, CategoryTheory.Limits.CompleteLattice.instHasBinaryProductsOfOrderTop, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow, AlgebraicGeometry.IsAffineOpen.fromSpec_top, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id, CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, CategoryTheory.Subobject.pullback_self, CategoryTheory.Abelian.SpectralObject.sc₃_X₃, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.Scheme.Hom.comp_appTop, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor_map, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_Q, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, CategoryTheory.ComposableArrows.isoMk₁_inv_app, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_one, SSet.horn₃₂.desc.multicofork_pt, AlgebraicGeometry.exists_map_eq_top, CategoryTheory.Abelian.SpectralObject.shortComplex_X₃, AlgebraicGeometry.Scheme.basicOpen_zero, InfiniteGalois.proj_of_le, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', CategoryTheory.nerve.ext_of_isThin_iff, CategoryTheory.Limits.CompleteLattice.instHasBinaryCoproductsOfOrderBot, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_zero, AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, CategoryTheory.Abelian.SpectralObject.sc₃_X₂, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, CategoryTheory.homOfLE_isIso_of_eq, CategoryTheory.SmallObject.restrictionLT_obj, CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_two, CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv, skyscraperPresheafCoconeOfSpecializes_ι_app, LightProfinite.Extend.functor_initial, TopologicalSpace.Opens.apply_mk, TopologicalSpace.Opens.infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.isFinite_iff, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, Fin.castSuccFunctor_map, Types.monoOverEquivalenceSet_unitIso, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, AlgebraicGeometry.etale_iff, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_map, CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit', CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, AlgebraicGeometry.Scheme.germ_residue_assoc, instIsContinuousOpensCarrierMapGrothendieckTopology, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom, AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, AlgebraicGeometry.Scheme.kerFunctor_obj, CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₃, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, CategoryTheory.SmallObject.restrictionLE_obj, AlgebraicGeometry.Scheme.Opens.ι_image_le, TopCat.Presheaf.Γgerm_res_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit, AlgebraicGeometry.Scheme.mem_basicOpen'', CategoryTheory.Triangulated.SpectralObject.triangle_obj₃, SimpleGraph.componentComplFunctor_nonempty_of_infinite, AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt, ProfiniteGrp.toLimitFun_continuous, CategoryTheory.Limits.CompleteLattice.limit_eq_iInf, CategoryTheory.GrothendieckTopology.diagramNatTrans_id, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE, CategoryTheory.ComposableArrows.isoMk₄_inv, AlgebraicGeometry.tilde.toOpen_map_app_assoc, CategoryTheory.ComposableArrows.mk₀_map, CategoryTheory.ComposableArrows.homMk₄_app_two, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit, CategoryTheory.Subobject.inf_comp_right, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_two, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc, TopologicalSpace.OpenNhds.map_id_obj, ProfiniteGrp.diagram_map, AlgebraicGeometry.Scheme.Opens.ι_appLE, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.Subobject.ofLEMk_comp_ofMkLE_assoc, AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc, CategoryTheory.SmallObject.restrictionLT_map, HomologicalComplex.HomologySequence.composableArrows₃Functor_map, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.Scheme.Hom.comp_image, CategoryTheory.SmallObject.SuccStruct.ofCocone_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.appLE_comp_appLE, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, InfiniteGalois.algEquivToLimit_continuous, AlgebraicGeometry.Scheme.Hom.resLE_appLE, TopCat.Presheaf.germ_stalkSpecializes, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top, CategoryTheory.Subobject.representative_coe, CategoryTheory.Limits.SequentialProduct.cone_π_app, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, AlgebraicGeometry.Scheme.Opens.ι_app, Opens.toPretopology_grothendieckTopology, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles, CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁', AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncGE, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc, CategoryTheory.Functor.ofSequence_obj, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.exists_basicOpen_le_affine_inter, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_three, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, CategoryTheory.Limits.kernelSubobject_arrow_apply, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, LightProfinite.Extend.functor_obj, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃, CategoryTheory.SmallObject.prop_iterationFunctor_map_succ, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, Set.functorToTypes_map, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality_assoc, CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, AlgebraicGeometry.Scheme.Hom.inv_image, AlgebraicGeometry.PresheafedSpace.restrict_presheaf, CategoryTheory.ComposableArrows.homMk_app, TopCat.Presheaf.germ_eq, CategoryTheory.Subobject.inf_eq_map_pullback, CategoryTheory.Equivalence.toOrderIso_symm_apply, CategoryTheory.Limits.imageSubobject_arrow_comp, AlgebraicGeometry.Scheme.germ_residue, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv, TopologicalSpace.Opens.map_top, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, LightProfinite.proj_surjective, CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁, CategoryTheory.Subfunctor.Subpresheaf.subobjectMk_range_arrow, AlgebraicGeometry.Scheme.Hom.opensRange_comp, CategoryTheory.eqToHom_comp_homOfLE_op_assoc, Topology.IsInducing.le_functorObj_iff, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₁, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, CategoryTheory.TransfiniteCompositionOfShape.map_incl, CategoryTheory.Limits.CompleteLattice.limitCone_cone_π_app, Set.Ici.subtype_functor_final, TopologicalSpace.Opens.overEquivalence_inverse_obj_right_as, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, imageToKernel_zero_left, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.Scheme.Hom.map_appLE, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, TopologicalSpace.Opens.apply_def, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₂, CategoryTheory.Triangulated.SpectralObject.triangle_obj₁, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ, AlgebraicGeometry.Scheme.Γevaluation_naturality, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₂, CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape, AlgebraicGeometry.IsSeparated.instMorphismRestrict, CategoryTheory.ComposableArrows.homMk₂_app_one, AlgebraicGeometry.basicOpen_eq_bot_iff, CategoryTheory.ComposableArrows.δ₀Functor_map_app, nonempty_sections_of_finite_inverse_system, CategoryTheory.homOfLE_comp_eqToHom_assoc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, TopologicalSpace.Opens.mapMapIso_counitIso, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, CategoryTheory.SmallObject.coconeOfLE_ι_app, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, TopologicalSpace.Opens.toTopCat_map, ProfiniteGrp.isIso_toLimit, CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT, CategoryTheory.ComposableArrows.homMk₅_app_four, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.quasiCompact_iff_forall_affine, skyscraperPresheafCoconeOfSpecializes_pt, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, CategoryTheory.Subobject.inf_pullback, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, HomologicalComplex.HomologySequence.composableArrows₃Functor_obj, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π, CategoryTheory.TransfiniteCompositionOfShape.map_F, TopCat.Presheaf.stalkFunctor_map_germ, CategoryTheory.ComposableArrows.sc'Map_τ₂, CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ, CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists, CategoryTheory.ComposableArrows.isoMk₀_hom_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', CategoryTheory.ComposableArrows.functorArrows_map, CategoryTheory.Subobject.inf_comp_right_assoc, CategoryTheory.Abelian.SpectralObject.liftCycles_i_assoc, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, CategoryTheory.nerveMap_app, TopCat.Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, OrderHom.equivFunctor_symm_apply, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, CategoryTheory.Subobject.lowerEquivalence_inverse, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, InfiniteGalois.limitToAlgEquiv_symm_apply, CategoryTheory.Subobject.lowerEquivalence_functor, AlgebraicGeometry.Scheme.preimage_basicOpen, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_bot, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, CategoryTheory.orderDualEquivalence_inverse_obj, CategoryTheory.Subfunctor.Subpresheaf.range_subobjectMk_ι, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_one, AlgebraicGeometry.IsAffineHom.isAffine_preimage, TopCat.Presheaf.toPushforwardOfIso_app, CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id, CategoryTheory.Abelian.SpectralObject.sc₁_X₂, AlgebraicGeometry.Scheme.Hom.flat_appLE, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.Scheme.comp_app_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, ModuleCat.directLimitCocone_pt_isModule, TopCat.Presheaf.restrict_sum, instHasBinaryProducts, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, SkyscraperPresheafFunctor.map'_app, CategoryTheory.Subobject.functor_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.morphismRestrict_app, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc, CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp, Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, PresheafOfModules.germ_ringCat_smul, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, OrderHom.equivalenceFunctor_unitIso_inv_app, ModuleCat.directLimitDiagram_map, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, TopCat.Sheaf.eq_of_locally_eq_iff, AlgebraicGeometry.exists_lift_of_germInjective_aux, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, CategoryTheory.Subobject.thinSkeleton_mk_representative_eq_self, imageToKernel_epi_of_epi_of_zero, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, CategoryTheory.Abelian.SpectralObject.sc₂_f, CategoryTheory.Triangulated.TStructure.eTruncGEδLT_coe, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.Scheme.Γ_obj_op, CategoryTheory.ComposableArrows.naturality'_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, SimpleGraph.componentComplFunctor_map, TopCat.Presheaf.IsSheaf.isSheafOpensLeCover, CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality, coverPreserving_opens_map, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, CategoryTheory.Subobject.finset_inf_arrow_factors, CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁, AlgebraicGeometry.Scheme.image_zeroLocus, AlgebraicGeometry.Scheme.Hom.appLE_map, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE, CategoryTheory.isFilteredOrEmpty_of_semilatticeSup, AlgebraicGeometry.Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, IsOpenMap.coe_functor_obj, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃', AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen, CategoryTheory.instCountableCategoryNat, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₃, AlgebraicGeometry.Proj.res_apply, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.CostructuredArrow.projectQuotient_factors, TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f, AlgebraicGeometry.Scheme.Opens.topIso_hom, CategoryTheory.Limits.kernelSubobject_arrow_comp, SimplexCategory.toCat_map, TopologicalSpace.Opens.overEquivalence_counitIso_hom_app, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc, AlgebraicGeometry.StructureSheaf.toOpen_res, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, CategoryTheory.Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, PresheafOfModules.germ_smul, AlgebraicGeometry.Scheme.zeroLocus_univ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, CategoryTheory.SmallObject.preservesColimit, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, AlgebraicGeometry.Scheme.Hom.image_le_image_iff, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv, CategoryTheory.ComposableArrows.functorArrows_obj, AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc, CategoryTheory.GrothendieckTopology.diagramNatTrans_zero, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.StructureSheaf.const_mul, AlgebraicGeometry.AffineSpace.map_appTop_coord, CategoryTheory.ComposableArrows.homMk₂_app_two', CategoryTheory.Subobject.map_obj_injective, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_obj, Fin.succFunctor_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_top, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT, CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.isIso_fromTildeΓ_iff, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.isFiltered_of_directed_le_nonempty, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso, CategoryTheory.GrothendieckTopology.preservesLimit_diagramFunctor, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_assoc, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_zero, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, SSet.horn₃₂.desc.multicofork_π_zero, CategoryTheory.isEventuallyConstant_of_isNoetherianObject, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.Scheme.zero_of_zero_cover, CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles_assoc, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_π_app, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj, CategoryTheory.Abelian.SpectralObject.sc₃_f, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, CategoryTheory.isNoetherianObject_iff_isEventuallyConstant, SSet.horn₃₂.desc.multicofork_π_three_assoc, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot, Types.monoOverEquivalenceSet_counitIso, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop, CategoryTheory.Subobject.instFaithfulPullback, CategoryTheory.Abelian.SpectralObject.zero₁_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj, SSet.horn₃₂.desc.multicofork_π_one_assoc, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, CategoryTheory.Subobject.underlyingIso_arrow_apply, AlgebraicGeometry.exists_of_res_eq_of_qcqs, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, TopCat.Presheaf.coveringOfPresieve_apply, TopCat.Sheaf.isLocallySurjective_iff_epi, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc, TopCat.subpresheafToTypes_obj, TopCat.Presheaf.submonoidPresheafOfStalk_obj, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom, TopCat.Presheaf.stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, CategoryTheory.ShortComplex.mapToComposableArrows_id, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, CategoryTheory.ComposableArrows.precomp_map, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, TopCat.GlueData.MkCore.cocycle, finGaloisGroupMap.map_comp, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₃, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_three, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, TopologicalSpace.OpenNhds.inclusionMapIso_inv_app, CategoryTheory.isArtinianObject_iff_isEventuallyConstant, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE, CategoryTheory.ThinSkeleton.map_comp_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₃, AlgebraicGeometry.map_injective_of_isIntegral, CategoryTheory.Subobject.underlying_arrow, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated, AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, HasCardinalLT.Set.isFiltered_of_aleph0_le, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, AlgebraicGeometry.Proj.stalkIso'_symm_mk, CategoryTheory.GrothendieckTopology.pullback_obj, AlgebraicGeometry.structureSheafInType.smul_apply, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁, Opens.instSubsingletonObjOpensFiber, TopologicalSpace.OpenNhds.apply_mk, AlgebraicGeometry.Etale.instMorphismRestrict, CategoryTheory.GrothendieckTopology.diagramNatTrans_comp, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id, CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, CategoryTheory.Abelian.SpectralObject.instMonoICycles, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, LightProfinite.proj_comp_transitionMap', AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, CategoryTheory.ComposableArrows.homMk₀_app, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isColimit, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ, AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, AlgebraicGeometry.RingedSpace.mem_basicOpen, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_three, AlgebraicGeometry.Scheme.Hom.app_injective, CategoryTheory.Functor.mapPresheaf_obj_presheaf, AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_map, CategoryTheory.Subobject.representative_arrow, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀, TopCat.Presheaf.mono_iff_stalk_mono, CategoryTheory.Limits.kernelSubobjectMap_arrow, AlgebraicGeometry.Scheme.Modules.inv_app, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁_assoc, TopCat.Presheaf.ext_iff, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, CategoryTheory.Abelian.SpectralObject.toCycles_descCycles_assoc, CategoryTheory.SubobjectRepresentableBy.iso_inv_left_π, SSet.horn₃₁.desc.multicofork_π_three, OrderIso.equivalence_unitIso, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁, Topology.IsOpenEmbedding.compatiblePreserving, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, ModuleCat.toKernelSubobject_arrow, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, CategoryTheory.Limits.imageSubobject_arrow', CategoryTheory.Subobject.factorThru_zero, TopCat.Presheaf.presheafEquivOfIso_functor_obj_map, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, CategoryTheory.Abelian.SpectralObject.map_comp_assoc, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom, AlgebraicGeometry.Scheme.stalkMap_germ, Condensed.instAB4CondensedMod, CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, Fin.succFunctor_map, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂, imageToKernel_comp_mono, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, CategoryTheory.Subobject.isoOfEqMk_hom, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, TopCat.Presheaf.stalkFunctor_map_germ_assoc, TopologicalSpace.OpenNhds.inclusionMapIso_hom_app, CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux, CategoryTheory.Limits.kernelSubobject_arrow', CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁, CategoryTheory.orderDualEquivalence_inverse_map, TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk, TopologicalSpace.Opens.mapIso_refl, CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_zero, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂_assoc, AlgebraicGeometry.Scheme.comp_appLE_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Proj.awayToSection_comp_appLE_assoc, CategoryTheory.Limits.CompleteLattice.coprod_eq_sup, AlgebraicGeometry.Scheme.Hom.eqToHom_app, CategoryTheory.ThinSkeleton.comp_toThinSkeleton, TopCat.presheafToTypes_obj, instRepresentablyFlatOpensCarrierMap, TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete, Profinite.isIso_asLimitCone_lift, AlgebraicGeometry.Scheme.id_app, CategoryTheory.ComposableArrows.homMk₁_app, CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInTypeOpBasicOpenPowersToOpenₗ, Alexandrov.projSup_map, AlgebraicGeometry.flat_iff, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂, CategoryTheory.Subobject.hasLimitsOfSize, Topology.IsInducing.functorNhds_map, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso, AlgebraicGeometry.Scheme.zeroLocus_map_of_eq, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le, LightProfinite.Extend.functorOp_final, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf, CategoryTheory.Localization.essSurj_mapComposableArrows, TopCat.Presheaf.sections_exact_of_exact, CategoryTheory.ComposableArrows.isIso_iff₁, CategoryTheory.Limits.factorThruImageSubobject_comp_self, TopologicalSpace.Opens.val_apply, CategoryTheory.Limits.instIsWellOrderContinuousCompOfPreservesWellOrderContinuousOfShape, AlgebraicGeometry.IsOpenImmersion.lift_app, CategoryTheory.nerve.δ₂_two, AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality, CategoryTheory.Abelian.SpectralObject.sc₁_g, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, germ_skyscraperPresheafStalkOfSpecializes_hom, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine, CategoryTheory.ComposableArrows.IsComplex.zero', AlgebraicGeometry.Scheme.IdealSheafData.le_def, Topology.IsInducing.functor_map, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom, TopCat.Presheaf.isSheaf_of_isOpenEmbedding, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, isGLB_of_isLimit, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₃, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, CategoryTheory.Meq.pullback_apply, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj, CategoryTheory.Subfunctor.subobjectMk_range_arrow, CategoryTheory.Dial.tensorObj_rel, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact, CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp, CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc, CategoryTheory.Subobject.hasFiniteLimits, CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'_hom, CategoryTheory.Subobject.map_id, skyscraperPresheaf_map, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, AlgebraicGeometry.Scheme.Modules.map_smul, AlgebraicGeometry.RingedSpace.mem_basicOpen', CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc, AlgebraicGeometry.Scheme.mem_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, CategoryTheory.ThinSkeleton.toThinSkeleton_faithful, Subobject.presheaf_map, CategoryTheory.SemilatticeInf.tensorObj, AlgebraicGeometry.SheafedSpace.comp_c_app', CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem_incl_app, SSet.stdSimplex.isoNerve_inv_app_apply, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, CategoryTheory.Limits.SequentialProduct.functorMap_commSq, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.IsAffineOpen.preimage, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, CategoryTheory.Abelian.SpectralObject.map_id, AlgebraicGeometry.LocallyRingedSpace.Γ_obj, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit, CategoryTheory.ComposableArrows.δlastFunctor_obj_map, AlgebraicGeometry.Spec.map_app, CategoryTheory.ComposableArrows.homMk₃_app_zero, AlgebraicGeometry.exists_lift_of_germInjective, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, CategoryTheory.Limits.pullback_equalizer, ProfiniteGrp.diagram_obj, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.morphismRestrict_id, CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt, AlgebraicGeometry.tilde.toOpen_map_app, CategoryTheory.ComposableArrows.Precomp.map_one_one, CategoryTheory.Limits.ColimitPresentation.self_ι, CategoryTheory.Triangulated.TStructure.spectralObject_δ, CategoryTheory.eqToHom_comp_homOfLE_assoc, TopologicalSpace.Opens.map_id_eq, AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, CategoryTheory.Limits.kernelSubobjectMap_id, CategoryTheory.Functor.mapComposableArrows_map_app, AlgebraicGeometry.Scheme.Hom.id_image, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingleton_hom 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct smallCategory	—	ULift.ext

Quiver.Hom

Definitions

Name	Category	Theorems
le 📖	CompOp	23 math math: AlgebraicGeometry.Scheme.Hom.resLE_map_assoc, TopCat.Presheaf.germ_res', TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.Scheme.Hom.resLE_map, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.Scheme.Hom.map_appLE_assoc, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, TopCat.Presheaf.germ_res_apply', TopCat.Presheaf.germ_res, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc, TopCat.Presheaf.germ_res'_assoc, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc, TopologicalSpace.Opens.apply_mk, AlgebraicGeometry.Scheme.appLE_comp_appLE, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, AlgebraicGeometry.Scheme.Hom.map_appLE, TopologicalSpace.Opens.apply_def, TopologicalSpace.Opens.toTopCat_map, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, ModuleCat.directLimitDiagram_map, AlgebraicGeometry.Scheme.Hom.appLE_map, TopologicalSpace.OpenNhds.apply_mk

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFullFunctor 📖	mathematical	—	CategoryTheory.Functor.Full Preorder.smallCategory Monotone.functor DFunLike.coe OrderEmbedding Preorder.toLE instFunLikeOrderEmbedding OrderEmbedding.monotone	—	OrderEmbedding.monotone RelEmbedding.map_rel_iff

---

← Back to Index