IsLocalization

📁 Source: Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean

Statistics

Metric	Count
Definitions IsLocalization, IsLocalization	2
Theorems mk'_algebraMap_eq_mk', mk'_eq_mk', instIsLocalizedModuleLinearMapOfIsLocalization, instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid, isLocalizedModule_iff_isLocalization, isLocalizedModule_iff_isLocalization'	6
Total	8

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsLocalization 📖	CompData	51 math math: DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.Localization.isLocalization_op, CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1, IsLocalization.for_id, IsLocalization.instDiscreteObjWhiskeringRightFunctorCategoryOfFiniteOfContainsIdentities, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CategoryTheory.ObjectProperty.isLocalization_isColocal, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, CategoryTheory.Localization.Construction.prodIsLocalization, CategoryTheory.Adjunction.isLocalization_rightAdjoint', IsLocalization.of_comp, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, CategoryTheory.MorphismProperty.HasLocalization.hL, IsLocalization.prod, CategoryTheory.Adjunction.isLocalization_leftAdjoint', CategoryTheory.ObjectProperty.isLocalization_isLocal, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.Adjunction.isLocalization, op_iff, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, IsLocalization.instCompOfIsEquivalence, CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsLocalizationQ, IsLocalization.of_iso, IsLocalization.op_iff, IsLocalization.of_equivalence_source, CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q', IsLocalization.of_isEquivalence, IsLocalization.comp, CategoryTheory.Adjunction.isLocalization', instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, IsLocalization.unop, CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW, IsLocalization.mk', CategoryTheory.FreeGroupoid.instIsLocalizationOfTopMorphismProperty, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, q_isLocalization, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization, ComplexShape.quotient_isLocalization, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences, CategoryTheory.Adjunction.isLocalization_leftAdjoint, CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory, IsLocalization.of_equivalence_target, IsLocalization.of_equivalences, IsLocalization.op, CategoryTheory.Localization.LeftBousfield.isLocalization, CategoryTheory.Adjunction.isLocalization_rightAdjoint, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk'_algebraMap_eq_mk' 📖	mathematical	—	mk' Algebra.algebraMapSubmonoid CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike DFunLike.coe RingHom RingHom.instFunLike algebraMap Algebra.mem_algebraMapSubmonoid_of_mem IsLocalizedModule.mk' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom.toLinearMap IsScalarTower.toAlgHom instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid	—	Algebra.mem_algebraMapSubmonoid_of_mem instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid IsLocalizedModule.mk'_cancel' Submonoid.smul_def algebraMap_smul smul_mk'_self
mk'_eq_mk' 📖	mathematical	—	mk' IsLocalizedModule.mk' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization	—	instIsLocalizedModuleLinearMapOfIsLocalization IsLocalizedModule.mk'_cancel' smul_mk'_self

(root)

Definitions

Name	Category	Theorems
IsLocalization 📖	MathDef	50 math math: IsLocalization.localization_localization_isLocalization_of_has_all_units, Localization.subalgebra.isLocalization_subalgebra, IsLocalization.isLocalization_iff_of_isLocalization, Localization.isLocalization_range_mapToFractionRing, IsLocalization.isLocalization_iff_of_ringEquiv, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, IsIntegralClosure.isLocalization, IsLocalization.commutes, IsLocalization.isLocalization_iff_of_base_ringEquiv, IsLocalization.self, IsLocalization.of_surjective, IsLocalization.Away.instMapRingHomPowersOfCoe, IsLocalization.of_le_of_exists_dvd, Algebra.essFiniteType_cond_iff, NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, isLocalizedModule_iff_isLocalization, isLocalization_iff, IsLocalization.iff_map_piEvalRingHom, IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap, IsLocalization.at_units, Localization.subalgebra.isLocalization_ofField, LaurentSeries.of_powerSeries_localization, Algebra.EssFiniteType.isLocalization, IsLocalization.isLocalization_of_submonoid_le, TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf, IsLocalization.isLocalization_of_base_ringEquiv, Localization.isLocalization, Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors, Polynomial.isLocalization, Algebra.essFiniteType_iff_exists_subalgebra, IsLocalization.isLocalization_iff_of_algEquiv, isLocalizedModule_iff_isLocalization', IsLocalization.tensorRight, IsLocalization.tensor, MvPolynomial.isLocalization, IsLocalization.integralClosure, IsLocalization.isLocalization_algebraMapSubmonoid_map_algHom, IsLocalization.localization_localization_isLocalization, IsLocalization.of_le, IsLocalization.isLocalization_of_algEquiv, instIsLocalizationIntPosRat, isLocalization_iff_isLocalizationMap, IsLocalization.iff_of_le_of_exists_dvd, Algebra.EssFiniteType.cond, instIsLocalizationAlgebraMapSubmonoid, IsLocalization.isLocalization_of_is_exists_mul_mem, IsLocalization.tensorProduct_tensorProduct, IsIntegralClosure.isLocalization_of_isSeparable, Algebra.isLocalization_iff_isPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizedModuleLinearMapOfIsLocalization 📖	mathematical	—	IsLocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Algebra.linearMap	—	isLocalizedModule_iff_isLocalization'
instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid 📖	mathematical	—	IsLocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule AlgHom.toLinearMap IsScalarTower.toAlgHom	—	isLocalizedModule_iff_isLocalization
isLocalizedModule_iff_isLocalization 📖	mathematical	—	IsLocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule AlgHom.toLinearMap IsScalarTower.toAlgHom IsLocalization Algebra.algebraMapSubmonoid	—	smulCommClass_self IsScalarTower.left isLocalizedModule_iff isLocalization_iff AlgHom.commutes Algebra.smul_def mul_comm
isLocalizedModule_iff_isLocalization' 📖	mathematical	—	IsLocalizedModule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Algebra.linearMap IsLocalization	—	IsScalarTower.left MonoidHom.instMonoidHomClass Submonoid.map_id isLocalizedModule_iff_isLocalization

---

← Back to Index