IsIso 📖 | CompData | 876 mathmath: FinitaryPreExtensive.isIso_sigmaDesc_fst, GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, Adjunction.Triple.isIso_unit_iff_isIso_counit, Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, Limits.coequalizer.π_of_self, Functor.isLeftKanExtension_iff_isIso, isIso_of_op, Grp.instIsIsoHomHomMon, isIso_sheafificationAdjunction_counit, Functor.isIso_of_isRightDerivedFunctor_of_inverts, Monad.algebra_iso_of_iso, Limits.image.isIso_precomp_iso, ComplexShape.Embedding.isIso_liftExtend_f_iff, AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage, conjugateEquiv_iso, ShortComplex.HomologyData.ofIso_right_p, Triangulated.TStructure.instIsIsoMapTruncLTTruncGEAppTruncLTι, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, Limits.isIso_ι_terminal, DerivedCategory.right_fac, Limits.equalizer.ι_of_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, NatTrans.isIso_app_iff_of_iso, Limits.CategoricalPullback.instIsIsoSnd, ShortComplex.isIso_leftHomologyπ, Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension, isIso_of_yoneda_map_bijective, isIso_homOfLE, Limits.colimitLimitToLimitColimit_isIso, Limits.isIso_prod, Triangulated.TStructure.instIsIsoMapTruncLTAppTruncLTι, Limits.isIso_cokernel_map_of_isPushout, isIso_of_fully_faithful, Limits.isIso_app_coconePt_of_preservesColimit, ComposableArrows.isIso_iff₂, AlgebraicGeometry.instIsIsoSchemeCoprodComparisonOppositeCommRingCatSpec, CondensedMod.IsSolid.isIso_solidification_map, AlgebraicGeometry.ΓSpec.isIso_adjunction_counit, isIso_of_coyoneda_map_bijective, Limits.isIso_π_of_isTerminal, MorphismProperty.isIso_fst'_self, ShortComplex.quasiIso_iff_isIso_rightHomologyMap', ShortComplex.isIso_homologyFunctor_map_of_epi_of_isIso_of_mono, Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, prodComparison_iso, MonoOver.isIso_left_iff_subobjectMk_eq, Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero, Pretriangulated.Triangle.instIsIsoHom₂, AlgebraicGeometry.isIso_SpecMap_iff, NatIso.isIso_app_of_isIso, ShortComplex.isIso_homologyMap_of_isIso_cyclesMap_of_epi, Adjunction.instIsIsoFunctorCounitOfIsEquivalence_1, Functor.instIsIsoAppRanCounit, Adjunction.instIsIsoAppCounitOfFullOfFaithful, IsIso.mk', MonoidalCategory.MonoidalLeftAction.isIso_actionHom, to_initial_isIso, Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, isIso_unop_iff, Functor.Monoidal.instIsIsoδ, CondensedMod.isDiscrete_tfae, MonoOver.isIso_iff_subobjectMk_eq, Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit', Functor.LeftLinear.instIsIsoδₗ, AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued, AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite, SSet.Truncated.sk_coreflective, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, IsIso.of_epi_section, isIso_of_reflects_iso, Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instIsIsoInvApp, Limits.pushout_inr_iso_of_left_iso, ShortComplex.isIso_iCycles, AlgebraicGeometry.Scheme.Hom.instIsIsoToNormalizationOfIsIntegralHom, Abelian.SpectralObject.isIso_map, Triangulated.TStructure.isIso_truncLE_map_truncLEι_app, Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, ObjectProperty.IsStrongGenerator.isIso_of_mono, IsSubterminal.isIso_diag, ShortComplex.exact_iff_isIso_imageToKernel', Arrow.isIso_of_isIso_left_of_isIso_right, Limits.pullback_snd_iso_of_left_iso, MorphismProperty.isomorphisms.iff, Limits.instIsIsoPushoutComparison, ShortComplex.isIso_homologyπ, Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app, Subobject.top_arrow_isIso, Functor.Monoidal.instIsIsoη, CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction, Functor.reflective', Comma.instIsIsoRight, IsIso.of_mono_retraction', isIso_of_isDiscrete, Adjunction.instIsIsoFunctorUnitOfIsEquivalence, LightCondMod.isDiscrete_tfae, ShortComplex.isIso_cyclesMap'_of_isIso_of_mono, IsPushout.isIso_inr_of_isIso, Triangulated.TStructure.isLE_iff_isIso_truncLEι_app, CompHausLike.isIso_of_bijective, StrictlyUnitaryLaxFunctor.mapId_isIso, IsHomLift.isIso_of_lift_isIso, ShortComplex.isIso_leftRightHomologyComparison, Limits.Cofan.isColimit_iff_isIso_sigmaDesc, IsIso.of_isIso_comp_left, ShortComplex.isIso_leftHomologyMap'_of_isIso, CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE, ShortComplex.isIso_cyclesMap_of_isIso_of_mono, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison, IsIso.instUnmopOfMonoidalOpposite, Presheaf.isIso_of_isLeftKanExtension, GrothendieckTopology.isIso_toSheafify, isIso_comp_right_iff, Limits.instIsIsoHomHomCocone, Limits.IsInitial.isIso_to, NonPreadditiveAbelian.isIso_factorThruCoimage, instIsIsoToRightDerivedZero', Triangulated.TStructure.isGE_iff_isIso_truncGTπ_app, Monad.isSplitMono_iff_isIso_unit, isIso_iff_coyoneda_map_bijective, Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull, Functor.isRightDerivedFunctor_iff_of_inverts, MonoidalCategory.MonoidalRightAction.isIso_actionHom, PreZeroHypercover.instIsIsoH₀Hom, ShortComplex.isIso_opcyclesMap'_of_isIso, ShortComplex.LeftHomologyData.isIso_i, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.Scheme.Modules.instIsIsoFunctorCounitRestrictAdjunction, Functor.ReflectsIsomorphisms.reflects, MonoidalClosedFunctor.comparison_iso, Limits.isIso_π_terminal, Limits.Pi.map_isIso, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, Limits.Cone.cone_iso_of_hom_iso, ShortComplex.ShortExact.isIso_g_iff, isIso_of_epi_of_strongMono, ShortComplex.isIso₂_of_shortExact_of_isIso₁₃', LocalizerMorphism.Derives.isIso, isIso_toSheafify, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, Limits.IsLimit.nonempty_isLimit_iff_isIso_lift, Limits.isIso_ι_of_isInitial, MonoOver.isIso_hom_left_iff_subobjectMk_eq, AlgebraicGeometry.isIso_iff_isIso_stalkMap, MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft, Functor.isIso_whiskerRight, Limits.kernelSubobject_comp_mono_isIso, Limits.CategoricalPullback.isIso_iff, ShortComplex.RightHomologyMapData.quasiIso_map_iff, Limits.pullback.instIsIsoDiagonalOfMono, NatIso.isIso_of_isIso_app, ShortComplex.isIso_leftRightHomologyComparison', Limits.isIso_of_isTerminal, Limits.HasZeroObject.zero_to_zero_isIso, HomologicalComplex.instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, Limits.instIsIsoTerminalComparison, Triangulated.TStructure.isIso_truncLT_map_iff, Limits.IsColimit.nonempty_isColimit_iff_isIso_desc, Presheaf.instIsIsoFunctorOfIsLeftKanExtensionOppositeType, Limits.pushout.instIsIsoCodiagonalOfEpi, Profinite.isIso_indexCone_lift, Limits.cokernel.π_zero_isIso, Limits.isIso_of_isInitial, Pretriangulated.Triangle.distinguished_iff_of_isZero₃, GradedObject.isIso_apply_of_isIso, TopCat.isIso_iff_isHomeomorph, Limits.instIsIsoMapOfMono, LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction, Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, Abelian.Preradical.IsIdempotent.isIso_whiskerLeft_r_ι, AlgebraicGeometry.isIso_fromTildeΓ_of_presentation, Limits.isIsoZero_iff_source_target_isZero, TopCat.fst_iso_of_right_embedding_range_subset, Limits.CatCospanTransform.instIsIsoWhiskerLeft, HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, GrothendieckTopology.preservesSheafification_iff_of_adjunctions, Limits.CokernelCofork.IsColimit.isIso_π, MorphismProperty.TransfiniteCompositionOfShape.isIso, CommGrp.instIsIsoMonHomGrp, Triangulated.TStructure.isIso_truncLT_map_truncLTι_app, instIsIsoFunctorOppositeSheafSheafComposeNatTrans, ShortComplex.Exact.isIso_imageToKernel, AlgebraicGeometry.Scheme.Hom.isIso_base, ShortComplex.isIso_pOpcycles, AlgebraicGeometry.IsOpenImmersion.isIso, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, isIso_iff_bijective, ShortComplex.exact_iff_isIso_imageToKernel, isIso_pi_iff, Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀, CommMon.instIsIsoHomHomMon, isIso_of_regularEpi_of_mono, Adjunction.instIsIsoFunctorCounitOfIsEquivalence, Abelian.SpectralObject.isIso_fromOpcycles, TopCat.GlueData.instIsIsoT, Pretriangulated.Triangle.distinguished_iff_of_isZero₁, Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT, IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver, GrothendieckTopology.W_iff_isIso_map_of_adjunction, Comonad.isSplitEpi_iff_isIso_counit, isIso_of_mono_of_nonzero, Limits.IsColimit.isIso_colimMap_ι, GlueData.f_id, Limits.isIso_limMap, ExtremalEpi.isIso, InjectiveResolution.instIsIsoToRightDerivedZero'Self, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso, Action.isIso_of_hom_isIso, PreOneHypercover.instIsIsoH₁Hom, SimplexCategory.isIso_iff_of_epi, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, Limits.IsIPC.isIso, DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso, IsIso.inv_isIso, Bicategory.conjugateEquiv_symm_of_iso, Pretriangulated.Triangle.isIso_of_isIsos, instIsIsoAppToRightDerivedZeroOfInjective, Triangulated.TStructure.instIsIsoAppTruncLEιOfIsLE, ShortComplex.QuasiIso.isIso, Triangulated.TStructure.instIsIsoMapTruncLEAppTruncLEι, ShortComplex.quasiIso_iff_isIso_homologyMap', Limits.isIso_limit_cone_parallelPair_of_epi, Adjunction.isIso_counit_of_iso, isIso_comp_left_iff, FinitaryPreExtensive.isIso_sigmaDesc_map, isIso_right_of_isIso_biprod_map, Limits.HasStrictTerminalObjects.out, Functor.instIsIsoAppLanUnit, SSet.S.mk_map_eq_iff_of_mono, isUnit_iff_isIso, Limits.HasStrictInitialObjects.out, Bicategory.instIsIsoHomLeftZigzagHom, AlgebraicGeometry.Spec_map_localization_isIso, Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, HomologicalComplex.isIso_homologyπ, ShortComplex.instIsIsoτ₃, TwoSquare.isIso_lanBaseChange_app, Adjunction.isIso_counit_app_of_iso, SimplexCategory.isIso_of_bijective, conjugateEquiv_symm_iso, Limits.Cocone.cocone_iso_of_hom_iso, Abelian.SpectralObject.isIso_toCycles, ObjectProperty.isLocal_iff_isIso, IsGrothendieckAbelian.IsPresentable.surjectivity.isIso_f, Endofunctor.Algebra.Initial.str_isIso, Subobject.Classifier.instIsIsoHom, Limits.CatCospanTransform.instIsIsoWhiskerRight, ShortComplex.instIsIsoτ₁, Pretriangulated.Triangle.distinguished_iff_of_isZero₂, Action.instIsIsoHomInv, ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData, Adjunction.instIsIsoAppUnitOfFullOfFaithful, HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g, CochainComplex.isIso_πTruncGE_iff, AlgebraicGeometry.isIso_stalkMap_coprodSpec, AlgebraicGeometry.PresheafedSpace.isIso_of_components, SimplexCategory.isIso_iff_of_mono, isIso_iff_isIso_yoneda_map, ShortComplex.quasiIso_iff_isIso_descOpcycles, isIso_of_hom_simple, Functor.essImage.counit_isIso, SSet.isIso_of_nonDegenerate, Limits.PullbackCone.isIso_fst_of_mono_of_isLimit, GradedObject.instIsIsoMapBifunctorMapMap, AlgebraicGeometry.Scheme.instIsIsoCommRingCatResidueFieldMapOfIsOpenImmersion, Comonad.coalgebra_iso_of_iso, isIso_op, Subobject.isIso_top_arrow, hoFunctor.isIso_prodComparison_of_stdSimplex, MorphismProperty.TransfiniteCompositionOfShape.instIsIsoAppIncl, GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, Limits.CatCospanTransform.isIso_base, AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat, AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom, Functor.isLeftDerivedFunctor_iff_of_inverts, OverClass.instIsIsoOverAsOverHom, HomologicalComplex.instIsIsoπTruncGEOfIsStrictlySupported, ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, Adjunction.whiskerRight_counit_iso_of_L_fully_faithful, ShortComplex.QuasiIso.isIso', FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, IsIso.of_isIso_comp_right, Bicategory.whiskerLeft_isIso, ShortComplex.isIso_cyclesMap_of_isIso_of_mono', AlgebraicGeometry.IsOpenImmersion.to_iso, Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt, AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso, Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, Functor.isIso_ranAdjunction_unit_app_iff, Pretriangulated.isIso₃_of_isIso₁₂, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, Limits.BinaryCofan.isColimit_iff_isIso_inl, Limits.cokernel.π_of_zero, Functor.final_iff_isIso_colimit_pre, Limits.CategoricalPullback.instIsIsoFst, instIsIsoAppFromLeftDerivedZeroOfProjective, GradedObject.isIso_of_isIso_apply, Triangulated.TStructure.isIso_truncGT_map_truncGTπ_app, Adjunction.isIso_unit_app_iff_mem_essImage, Pretriangulated.Triangle.isZero₂_iff_isIso₃, ShortComplex.LeftHomologyMapData.quasiIso_map_iff, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective, ObjectProperty.isColocal_iff_isIso, Pretriangulated.Triangle.isZero₃_iff_isIso₁, IsIso.comp_isIso, AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, ShortComplex.instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth, IsIso.of_isIso_fac_right, ChainComplex.isIso_descOpcycles_iff, AlgebraicGeometry.isIso_iff_isOpenImmersion, Limits.KernelFork.IsLimit.isIso_ι, Subfunctor.eq_top_iff_isIso, Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison, Functor.OplaxMonoidal.instIsIsoη, IsPullback.isIso_snd_iso_of_mono, instIsIsoIndCoimageImageComparison, NatTrans.isIso_iff_isIso_app, FundamentalGroupoidFunctor.instIsIsoFunctorFundamentalGroupoidHomotopicMapsNatIso, Limits.instIsIsoEqualizerComparison, Limits.kernel.ι_of_zero, Limits.PushoutCocone.isIso_inl_of_epi_of_isColimit, Functor.Monoidal.instIsIsoμ, NonPreadditiveAbelian.isIso_r, instIsIsoHomologyMapOfQuasiIsoAt, Pretriangulated.Triangle.instIsIsoHom₃, ComposableArrows.Exact.isIso_map', Presheaf.isLeftKanExtension_along_uliftYoneda_iff, Limits.BinaryCofan.isColimit_iff_isIso_inr, Functor.IsEventuallyConstantTo.isIso_map, PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso, Limits.instIsIsoKernelComparison, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.tilde.isIso_toOpen_top, Limits.IsTerminal.isIso_from, Functor.IsStronglyCartesian.isIso_of_base_isIso, strict_initial, Arrow.isIso_left, Arrow.isIso_hom_iff_isIso_of_isIso, Limits.pushout_inr_iso_of_right_factors_epi, IsIso.of_isIso_fac_left, AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec, instIsIsoEqToHom, Limits.Cocones.cone_iso_of_hom_iso, Limits.isIso_colimit_cocone_parallelPair_of_eq, isIso_of_comp_hom_eq_id, PreGaloisCategory.FibreFunctor.end_isIso, AlgebraicGeometry.PresheafedSpace.stalkMap.isIso, IsGroupoid.all_isIso, HomologicalComplex.isIso_ιTruncLE_iff, conjugateEquiv_symm_of_iso, TwoSquare.isIso_lanBaseChange_app_iff, TwoSquare.instIsIsoFunctorLanBaseChangeOfGuitartExact, isIso_iff_nonzero, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor, Discrete.instIsIso, frobeniusMorphism_iso_of_preserves_binary_products, Limits.instIsIsoProdComparison, Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, ShortComplex.isIso_homologyι, Abelian.Preradical.isRadical_iff_isIso, Limits.isIso_ι_initial, ShortComplex.SnakeInput.isIso_δ, AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit, IsPushout.isIso_inr_iso_of_epi, Limits.pushout.isIso_codiagonal_iff, Abelian.isIso_of_isIso_of_mono, Pretriangulated.isIso₂_of_isIso₁₃, SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_app, Arrow.isIso_iff_isIso_of_isIso, Functor.RightExtension.IsPointwiseRightKanExtension.isIso_hom, PreGaloisCategory.isIso_of_mono_of_eq_card_fiber, Functor.isIso_ranAdjunction_homEquiv_iff, Functor.isIso_of_isLeftDerivedFunctor_of_inverts, Functor.essImage.unit_isIso, IsPullback.isIso_snd_of_isIso, AlgebraicGeometry.isIso_of_isEmpty, ObjectProperty.SerreClassLocalization.isIso_map_iff, HomologicalComplex.isIso_truncLE'ToRestriction, Limits.instIsIsoCoprodComparison, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso, BasedNatIso.isIso_of_toNatTrans_isIso, isIso_of_mono_of_strongEpi, isIso_left_of_isIso_biprod_map, Limits.Cocone.isColimit_iff_isIso_colimMap_ι, Presheaf.isSheaf_iff_multiequalizer, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful, Endofunctor.Coalgebra.iso_of_iso, ShortComplex.isIso_of_isIso, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsIsoCommRingCatInvApp, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, Limits.instIsIsoHomInvCone, Functor.RightLinear.instIsIsoμᵣ, Iso.isIso_inv, Limits.IsZero.isIso, Limits.instIsIsoCokernelComparison, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, Adjunction.unit_isIso_of_L_fully_faithful, HomologicalComplex.isIso_iCycles, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, ObjectProperty.isStrongGenerator_iff, instIsIsoAppUnitReflectorAdjunctionObjEssImage, CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits, Abelian.Preradical.instIsIsoMapRAppιOfIsIdempotent, Triangulated.TStructure.isIso₂_truncGT_map_of_isLE, Functor.RightLinear.instIsIsoδᵣ, TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso, AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso, TopCat.isIso_of_bijective_of_isOpenMap, TopCat.snd_iso_of_left_embedding_range_subset, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, Sheaf.isConstant_iff_isIso_counit_app', CochainComplex.isIso_liftCycles_iff, Limits.isIso_fst_of_mono, Limits.isIso_limit_cone_parallelPair_of_eq, Triangulated.TStructure.isIso_eTruncLTLTIsoLT, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, isIso_unop, Iso.isIso_hom, Limits.pullback_snd_iso_of_left_factors_mono, AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq, Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app, HomologicalComplex.isIso_πTruncGE_iff, ShortComplex.instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, ShortComplex.ShortExact.isIso_δ, PartialOrder.isIso_iff_eq, Abelian.Preradical.isIso_toColon_hom_left_app_iff, Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify, MonoidalCategory.whiskerRight_isIso, regularTopology.equalizerCondition_iff_isIso_lift, LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, Limits.pushout_inl_iso_of_left_factors_epi, Simple.mono_isIso_iff_nonzero, Action.instIsIsoHomHom, Pretriangulated.Triangle.instIsIsoHom₁, ShortComplex.isIso_rightHomologyMap_of_iso, PreZeroHypercover.instIsIsoH₀Inv, Monoidal.Reflective.instIsIsoAppUnitObjIhom, Subfunctor.instIsIsoFunctorTypeιTop, Functor.isIso_lanAdjunction_homEquiv_symm_iff, AlgebraicGeometry.Scheme.instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat, Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app, Triangulated.TStructure.isIso₂_truncGE_map_of_isLE, ShortComplex.isIso_rightHomologyMap'_of_isIso, Limits.colimitLimitToLimitColimitCone_iso, Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom, Subfunctor.instIsIsoFunctorTypeToRangeOfMono, Subobject.mk_lt_mk_iff_of_comm, Endofunctor.Coalgebra.Terminal.str_isIso, hoFunctor.isIso_prodComparison_stdSimplex, AlgebraicGeometry.IsClosedImmersion.isIso_lift, instIsIsoOverInferInstanceOverClass, Limits.instIsIsoEqToHom, isIso_iff_of_reflects_iso, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF, Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi, Balanced.isIso_of_mono_of_epi, ShortComplex.isIso_rightHomologyι, NatIso.hom_app_isIso, Limits.IsLimit.isIso_limMap_π, Limits.kernel.ι_zero_isIso, AlgebraicGeometry.Scheme.Hom.isIso_app, MonoOver.isIso_iff_isIso_hom_left, AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf, Adjunction.isIso_unit_of_iso, Coyoneda.isIso, ShortComplex.ShortExact.isIso_f_iff, ObjectProperty.IsDetecting.isIso_iff_of_mono, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, Arrow.isIso_hom_iff_isIso_hom_of_isIso, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.to_iso, ShortComplex.Exact.isIso_g', Limits.instIsIsoSigmaComparison, CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE, ConcreteCategory.isIso_iff_bijective, quasiIsoAt_iff_isIso_homologyMap, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, Triangulated.TStructure.isIso_truncGT_map_iff, isIso_iff_mono_and_epi, ShortComplex.isIso_homologyMap'_of_epi_of_isIso_of_mono, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, ObjectProperty.isColocal_iff_isIso_map, AlgebraicGeometry.IsClosedImmersion.isIso_of_ker_eq, CartesianMonoidalCategory.instIsIsoFunctorProdComparisonNatTransOfProdComparison, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, Functor.IsEventuallyConstantTo.isIso_π_of_isLimit, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom, HomotopyCategory.mem_quasiIso_iff, Triangulated.TStructure.isIso_truncGE_map_truncGEπ_app, Limits.isIso_kernelSubobject_zero_arrow, ShortComplex.instIsIsoτ₂, Arrow.isIso_of_isIso, IsPullback.isIso_fst_of_mono, CondensedSet.isDiscrete_tfae, Limits.instIsIsoPullbackComparison, Limits.CatCospanTransform.isIso_left, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, Triangulated.TStructure.isIso₁_truncLE_map_of_isGE, PreGaloisCategory.IsConnected.noTrivialComponent, Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀', TopCat.isIso_of_bijective_of_isClosedMap, IsDetecting.isIso_iff_of_mono, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, instIsIsoAppToRightDerivedZero, ShortComplex.isIso_homologyMap_of_isIso, Limits.pullback.isIso_diagonal_iff, localization_unit_isIso, Adjunction.counit_isIso_of_R_fully_faithful, ShortComplex.isIso₂_of_shortExact_of_isIso₁₃, Functor.IsCoverDense.iso_of_restrict_iso, MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft, MorphismProperty.LeftFraction.Localization.instIsIsoQinv, isIso_of_mono_of_isSplitEpi, ShortComplex.RightHomologyData.isIso_ι, PreOneHypercover.instIsIsoH₀Inv, TopCat.Presheaf.isIso_of_stalkFunctor_map_iso, Limits.BinaryFan.isLimit_iff_isIso_fst, Triangulated.TStructure.isIso₁_truncLT_map_of_isGE, HomologicalComplex.isIso_pOpcycles, instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, Functor.relativelyRepresentable.instIsIsoSymmetryOfFaithful, MorphismProperty.Comma.instIsIsoCommaHom, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, Bicategory.conjugateEquiv_of_iso, JointlyReflectIsomorphisms.isIso, Limits.instIsIsoInitialComparison, IsGrothendieckAbelian.generatingMonomorphisms.exists_pushouts, instIsIsoPost_1, Limits.kernel.of_cokernel_of_epi, GlueData.t_isIso, Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, Localization.LeftBousfield.W_iff_isIso, ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀, Triangulated.TStructure.instIsIsoMapTruncGEAppTruncGEπ, LocalizerMorphism.isIso_iff_of_hasRightResolutions, OrthogonalReflection.isIso_toSucc_iff, ShortComplex.Exact.isIso_f', AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, PreOneHypercover.instIsIsoH₀Hom, instIsIsoFunctorToRightDerivedZero, Functor.reflective, CommGrp.instIsIsoGrpHom, ShortComplex.isIso_opcyclesMap_of_iso, IsCodetecting.isIso_iff_of_epi, ChainComplex.isIso_homologyι₀, Biprod.isIso_inl_iff_isZero, ObjectProperty.IsConservativeFamilyOfPoints.W_iff, ObjectProperty.isLocal_iff_isIso_map, ShortComplex.instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, isCodetector_def, ShortComplex.quasiIso_iff, Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull, Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀', ComposableArrows.isIso_iff₀, ShortComplex.RightHomologyData.isIso_p, Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', Triangulated.TStructure.isIso_truncLE_map_iff, Limits.pullback_snd_iso_of_right_factors_mono, SimplicialObject.Truncated.cosk_reflective, Functor.Final.colimit_pre_isIso, isIso_of_regularMono_of_epi, DerivedCategory.right_fac_of_isStrictlyLE, ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, Functor.FullyFaithful.isIso_of_isIso_map, Functor.Monoidal.instIsIsoε, Limits.pushout_inl_iso_of_right_iso, IsIso.of_mono_retraction, Limits.Cone.isLimit_iff_isIso_limMap_π, expComparison_iso_of_frobeniusMorphism_iso, Limits.terminal_isIso_from, TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, isIso_iff_yoneda_map_bijective, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, Subobject.isIso_arrow_iff_eq_top, instIsIsoAppFromLeftDerivedZero, IsCodetector.def, Sieve.functorInclusion_top_isIso, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, Limits.equalizer.ι_of_self, Bicategory.conjugateEquiv_symm_iso, CompHausLike.isIsoSigmaComparison, HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv, NatIso.isIso_map_iff, ShortComplex.isIso_opcyclesMap_of_isIso_of_epi', isIso_of_epi_of_nonzero, Bicategory.instIsIsoHomRightZigzagHom, ShortComplex.isIso_leftHomologyMap_of_iso, HomologicalComplex.HomologySequence.isIso_homologyMap_τ₃, SheafOfModules.instIsIsoPullbackObjUnitToUnitOfFinal, GrothendieckTopology.W_iff, Endofunctor.Algebra.iso_of_iso, NatIso.inv_app_isIso, δ_iso_of_coreflective, PrelaxFunctor.map₂_isIso, Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, LightProfinite.isIso_of_bijective, ShortComplex.isIso_homologyMap_of_isIso_opcyclesMap_of_mono, Adjunction.isIso_map_unit_of_isLeftAdjoint_comp, SimplicialObject.Truncated.sk_coreflective, AlgebraicGeometry.IsAffine.affine, Functor.map_isIso, IsKernelPair.isIso_of_mono, Triangulated.TStructure.isIso_eTruncGEIsoGEGE, Limits.initial_isIso_to, isIso_of_mono_of_epi, PreOneHypercover.instIsIsoH₁Inv, Limits.IsColimit.hom_isIso, AlgebraicGeometry.Scheme.isIso_subschemeι_iff_eq_bot, ShortComplex.LeftHomologyData.isIso_π, ShortComplex.isIso_homologyMap_of_iso, Sheaf.isLocallyBijective_iff_isIso, AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso, Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc, HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported, Limits.Sigma.map_isIso, Limits.isIso_π_of_isInitial, instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, Functor.isRightKanExtension_iff_isIso, Triangulated.TStructure.instIsIsoFunctorTruncGELTToLTGE, Limits.Fan.nonempty_isLimit_iff_isIso_piLift, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left, ComposableArrows.Exact.isIso_cokerToKer', JointlyReflectIsomorphisms.isIso_iff, AlgebraicGeometry.isIso_pushoutSection_iff, isIso_iff_isIso_coyoneda_map, Limits.isIso_of_source_target_iso_zero, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve, ShortComplex.LeftHomologyMapData.quasiIso_iff, Limits.instIsIsoCoequalizerComparison, Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀', Limits.IsColimit.isIso_ι_app_of_isTerminal, Adjunction.isIso_unit_app_of_iso, AlgebraicGeometry.isIso_iff_stalk_iso, SSet.Truncated.cosk_reflective, LocalizerMorphism.Derives.isRightDerivedFunctor_iff_isIso, LocalizerMorphism.isIso_iff_of_isRightDerivabilityStructure, Abelian.Preradical.instIsIsoAppιObjROfIsIdempotent, instIsIsoFunctorFromLeftDerivedZero, AlgebraicGeometry.Scheme.Hom.isIso_toPshHom, CochainComplex.isIso_ιTruncLE_iff, Subobject.isIso_iff_mk_eq_top, AlgebraicGeometry.Flat.isIso_of_surjective_of_mono, Bicategory.whiskerRight_isIso, MorphismProperty.Comma.instIsIsoHomFromCommaOfIsIso, μ_iso_of_reflective, Limits.instIsIsoPiComparison, Limits.PullbackCone.isIso_snd_of_mono_of_isLimit, Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE, AddMon.instIsIsoHom, groupHomology.isIso_δ_of_isZero, AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop, homOfLE_isIso_of_eq, HomologicalComplex.isIso_restrictionToTruncGE', GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId, LightCondSet.isDiscrete_tfae, epi_iff_isIso_inl, AlgebraicGeometry.instIsIsoSchemeCoprodSpec, Triangulated.TStructure.isLE_iff_isIso_truncLTι_app, frobeniusMorphism_iso_of_expComparison_iso, isIso_of_epi_of_isSplitMono, Limits.limit_π_isIso_of_is_strict_terminal, BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor, Abelian.isIso_of_epi_of_isIso, Limits.isIso_inr_of_epi, Limits.Cone.instIsIsoExtendHom, IsDetector.def, Functor.IsEventuallyConstantFrom.isIso_map, Functor.isIso_whiskerLeft, ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono', Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, SingleFunctors.instIsIsoFunctorHom, Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁', ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono, Functor.instIsIsoAppLanUnit_1, IsIso.of_epi_section', Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt, Limits.isIso_coprod, Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc, ShortComplex.isIso_cyclesMap'_of_isIso, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, hom_isIso, Comma.instIsIsoLeft, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, ShortComplex.isIso_opcyclesMap_of_isIso_of_epi, Mon.instIsIsoHom, ShortComplex.quasiIso_iff_isIso_leftHomologyMap', Functor.IsEventuallyConstantTo.isIso_π_of_isLimit', Functor.IsStronglyCocartesian.isIso_of_base_isIso, IsIso.of_groupoid, Sieve.uliftFunctorInclusion_top_isIso, GrothendieckTopology.Point.instIsIsoηFunctorOppositePresheafFiber, ShortComplex.isIso_homologyMap'_of_isIso, Abelian.isIso_factorThruImage, localization_unit_isIso', NonPreadditiveAbelian.isIso_factorThruImage, ProfiniteGrp.isIso_toLimit, SimplicialObject.isCoskeletal_iff_isIso, Functor.LeftLinear.instIsIsoμₗ, AlgebraicGeometry.SheafedSpace.is_presheafedSpace_iso, ShortComplex.isIso_cyclesMap_of_iso, IsPullback.isIso_fst_of_isIso, Limits.isIso_π_initial, GlueData.t'_isIso, IsIso.comp_isIso', Limits.instIsIsoHomInvCocone, Limits.isIso_kernel_map_of_isPullback, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, Limits.isIso_colimit_cocone_parallelPair_of_self, MonoidalCategory.tensor_isIso, Limits.instIsIsoDescι, Functor.coreflective', Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit, sheafification_reflective, AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, Comon.instIsIsoHomOfMapForget, Limits.pullback_fst_iso_of_right_iso, AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top, Center.isIso_of_f_isIso, Limits.isIso_snd_of_mono, AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat, AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right, conjugateEquiv_of_iso, mono_iff_isIso_fst, ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁, RelCat.rel_iso_iff, Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃', AlgebraicGeometry.isIso_toSpecΓ, Adjunction.whiskerRight_unit_iso_of_R_fully_faithful, Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, Mon.instIsIsoHomOfMapForget, Bicategory.conjugateEquiv_iso, Sheaf.isLocallySurjective_iff_isIso, ShortComplex.Exact.isIso_imageToKernel', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, Abelian.Preradical.isIso_toColon_iff, Limits.CatCospanTransform.isIso_right, Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT, IsPushout.isIso_inl_iso_of_epi, ObjectProperty.IsCodetecting.isIso_iff_of_epi, Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post, instIsIsoF', Yoneda.isIso, Functor.Initial.limit_pre_isIso, Abelian.instIsIsoCoimageImageComparison, ShortComplex.Exact.isIso_toCycles, ShortComplex.instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, WithInitial.isIso_of_to_star, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, AlgebraicGeometry.isIso_fromTildeΓ_iff, IsIso.instMonoidalOppositeMop, Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃, mono_iff_isIso_snd, Functor.isLeftDerivedFunctor_iff_isIso_leftDerivedLift, AddMon.instIsIsoHomOfMapForget, Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull, isIso_prod_iff, Limits.PushoutCocone.isIso_inr_of_epi_of_isColimit, Action.isIso_hom_mk, Limits.BinaryFan.isLimit_iff_isIso_snd, Cat.Hom.instIsIsoFunctorαCategoryToNatTransHomHom, Subfunctor.Subpresheaf.eq_top_iff_isIso, HomologicalComplex.isIso_homologyι, Sheaf.isConstant_iff_isIso_counit_app, Triangulated.TStructure.instIsIsoAppTruncLTιObjTruncGETruncLT, MonoidalCategory.MonoidalRightAction.isIso_actionHomRight, DerivedCategory.isIso_Q_map_iff_quasiIso, DerivedCategory.isIso_Qh_map_iff, Limits.pullback.map_isIso, TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, Limits.CatCospanTransform.isIso_iff, CochainComplex.isIso_homologyπ₀, hoFunctor.isIso_prodComparison, Functor.isIso_lanAdjunction_counit_app_iff, Limits.Cones.cone_iso_of_hom_iso, Adjunction.isIso_counit_app_iff_mem_essImage, DerivedCategory.left_fac_of_isStrictlyGE, Abelian.isIso_factorThruCoimage, SmallObject.instIsIsoRightAppArrowιIteration, HomologicalComplex.isIso_π_f_of_isLimit_of_isEventuallyConstantTo, Limits.Types.isIso_colimitPointwiseProductToProductColimit, Pretriangulated.Triangle.isZero₁_iff_isIso₂, Functor.coreflective, Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullHom'Hom, LocalizerMorphism.isIso_iff_of_hasLeftResolutions, instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, Limits.isIso_limit_cone_parallelPair_of_self, nerveAdjunction.isIso_counit, isDetector_def, isIso_of_hom_comp_eq_id, Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeUliftYoneda, Limits.instIsIsoMapOfEpi, epi_iff_isIso_inr, Triangulated.TStructure.instIsIsoAppTruncGEπOfIsGE, Limits.pushout.map_isIso, GrothendieckTopology.isIso_toPlus_of_isSheaf, IsIso.id, Functor.instIsIsoAppRanCounit_1, Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Limits.Cocone.instIsIsoExtendHom, Pretriangulated.isIso₁_of_isIso₂₃, Limits.IsLimit.isIso_π_app_of_isInitial, Limits.isIso_inl_of_epi, HomologicalComplex.Hom.isIso_of_components, Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful, Localization.LeftBousfield.W_iff_isIso_map, Profinite.isIso_asLimitCone_lift, HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso, ShortComplex.Exact.isIso_fromOpcycles, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, LocalizerMorphism.isIso_α_iff_of_isRightDerivabilityStructure, Limits.coequalizer.π_of_eq, IsPushout.isIso_inl_of_isIso, LocalizerMorphism.instIsIsoFunctorRightDerivedFunctorComparison, ComposableArrows.isIso_iff₁, instIsIsoPost, ShortComplex.isIso_iff, isIso_op_iff, MonoidalCategory.whiskerLeft_isIso, Limits.IsLimit.hom_isIso, AlgebraicGeometry.IsClosedImmersion.isIso_of_injective_of_isAffine, GrpObj.instIsIsoInv, Limits.isIso_limit_cocone_parallelPair_of_epi, Functor.mem_homologicalKernel_trW_iff, Limits.instIsIsoHomHomCone, AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen, Limits.cokernel.of_kernel_of_mono, DerivedCategory.left_fac, SSet.Subcomplex.instIsIsoToRangeOfMono, Limits.isIso_ι_of_isTerminal, CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp, Triangulated.TStructure.isIso_truncGE_map_iff, Reflective.instIsIsoAppUnitReflectorAdjunctionA, groupCohomology.isIso_δ_of_isZero, Monoidal.Reflective.instIsIsoMapTensorHomAppUnit, Arrow.isIso_right, Limits.isIso_colimMap, Functor.OplaxMonoidal.instIsIsoδ, MonoOver.isIso_iff_isIso_left, instIsIsoFromLeftDerivedZero', ShortComplex.RightHomologyMapData.quasiIso_iff, MonoOver.instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono, ShortComplex.quasiIso_iff_isIso_liftCycles, FGModuleCat.instIsIsoCoimageImageComparison, WithTerminal.isIso_of_from_star, CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison, PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_initial, Discrete.instIsIsoFunctorNatTrans, MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight
|