Localization 📖 | CompOp | 190 mathmath: PrimeSpectrum.mapPiLocalization_id, Module.Finite.instLocalizationLocalizedModule, Submonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelMul, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, ModuleCat.localizedModule_functor_map_exact, Localization.epi', instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.mk_le_mk, Localization.mk_eq_monoidOf_mk', HomogeneousLocalization.val_nsmul, LocalizedModule.restrictScalars_map_eq, Module.Flat.localizedModule, Localization.instIsMulTorsionFree, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Localization.mk_eq_mk', Localization.algEquiv_apply, Module.freeLocus_localization, Module.FinitePresentation.exists_notMem_bijective, Localization.algEquiv_mk', Localization.mulEquivOfQuotient_symm_monoidOf, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, Localization.liftOn_zero, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.mk_algebraMap, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.AtPrime.isLocalRing, IsLocalization.instIsNoetherianRingLocalization, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, LocalizedModule.map_surjective, HomogeneousLocalization.val_zero, ModuleCat.instAdditiveLocalizationLocalizedModule_functor, HomogeneousLocalization.val_one, Algebra.FormallyEtale.instLocalization, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, Localization.mkOrderEmbedding_apply, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, Localization.algHom_ext_iff, Localization.isOrderedCancelMonoid, HomogeneousLocalization.val_injective, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, HomogeneousLocalization.val_smul, Localization.toLocalizationMap_eq_monoidOf, LocalizedModule.map_injective, HomogeneousLocalization.val_pow, LocalizedModule.equivTensorProduct_symm_apply_tmul, PrimeSpectrum.mapPiLocalization_bijective, HomogeneousLocalization.val_zsmul, Localization.mk_intCast, Localization.epi, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, HomogeneousLocalization.val_awayMap, Localization.liftOn₂_mk', IsLocalization.instIsScalarTowerLocalizationAtPrime, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', Localization.mk_one_eq_monoidOf_mk, PrimeSpectrum.mapPiLocalization_comp, ModuleCat.localizedModule_isLocalizedModule, Localization.algEquiv_mk, isIntegral_localization', ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor, Localization.mkHom_surjective, AlgebraicGeometry.Spec_map_localization_isIso, Localization.mulEquivOfQuotient_mk, Localization.mk_eq_mk'_apply, Localization.mk_sum, LocalizedModule.coe_map_eq, HomogeneousLocalization.val_sub, ModuleCat.localizedModule_functor_map, Localization.mapPiEvalRingHom_bijective, Localization.mk_eq_monoidOf_mk'_apply, Module.FinitePresentation.exists_free_localizedModule_powers, Localization.instNoZeroDivisors, PrimeSpectrum.mapPiLocalization_naturality, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization, HomogeneousLocalization.zero_eq, Localization.AtPrime.comap_maximalIdeal, Algebra.GrothendieckGroup.inv_mk, Localization.mulEquivOfQuotient_mk', PrimeSpectrum.toPiLocalization_bijective, HomogeneousLocalization.val_mul, instFinitePresentationLocalizationLocalizedModule, HomogeneousLocalization.val_add, Localization.mkAddMonoidHom_apply, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, Localization.algEquiv_symm_mk', HomogeneousLocalization.val_intCast, IsLocalization.isDomain_localization, Algebra.GrothendieckGroup.mk_div_mk, HomogeneousLocalization.val_natCast, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, instIsTopologicalRingLocalization, Localization.algEquiv_symm_mk, Localization.fg, Localization.mk_one_eq_algebraMap, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, Localization.mulEquivOfQuotient_symm_mk, Algebra.instEssFiniteTypeLocalization, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, Localization.mk_natCast, Localization.mk_list_sum, Localization.monoidOf_eq_algebraMap, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1, PrimeSpectrum.piLocalizationToMaximal_surjective, Localization.mk_self, HomogeneousLocalization.one_eq, Module.FinitePresentation.linearEquivMapExtendScalars_apply, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, Localization.isLocalization, instIsReducedLocalization, IsArtinianRing.instLocalization, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, Localization.mk_prod, HomogeneousLocalization.isUnit_iff_isUnit_val, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, Algebra.FormallySmooth.instLocalization, Localization.mk_one, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, LocalizedModule.map_id, Localization.smul_mk, IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.coe_algEquiv, Localization.mk_pow, Localization.mulEquivOfQuotient_monoidOf, LocalizedModule.algebraMap_mk, Localization.mulEquivOfQuotient_apply, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, Submonoid.LocalizationMap.instSubsingletonLocalization, HomogeneousLocalization.val_neg, Surreal.dyadicMap_apply, HomogeneousLocalization.Away.eventually_smul_mem, Localization.add_mk, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, Module.Invertible.instLocalizationLocalizedModule, IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, ModuleCat.localizedModuleMap_hom_apply, Localization.mkHom_apply, ModuleCat.localizedModule_functor_obj, HomogeneousLocalization.den_smul_val, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower, LocalizedModule.mk_smul_mk, WittVector.exists_frobenius_solution_fractionRing_aux, Localization.neg_mk, Localization.mk_mul, ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor, Localization.mk_lt_mk, Localization.mk_multiset_sum, LocalizedModule.smul_eq_iff_of_mem, IsLocalization.isLocalization_atPrime_localization_atPrime, exists_bijective_map_powers, LocalizedModule.map_mk, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, instIsScalarTowerLocalizationAlgebraMapSubmonoid, PrimeSpectrum.piLocalizationToMaximal_bijective, Localization.cardinalMk_le, PrimeSpectrum.toPiLocalization_injective, IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul, Localization.mk_left_injective, Submonoid.LocalizationMap.instIsCancelMulLocalization, Algebra.GrothendieckGroup.lift_apply, instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.flat, Localization.liftOn_mk', IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Localization.mk_self_mk, Localization.mulEquivOfQuotient_symm_mk', instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, Localization.mk_zero, Localization.AtPrime.map_eq_maximalIdeal, Surreal.dyadicMap_apply_pow, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.sub_mk, HomogeneousLocalization.algebraMap_apply, Localization.cardinalMk, Module.FinitePresentation.exists_basis_localizedModule_powers, Localization.add_mk_self, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, Algebra.QuasiFinite.instLocalization, Algebra.FormallyUnramified.instLocalization, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, Localization.coe_algEquiv_symm, Localization.algEquiv_symm_apply
|