Locally

📁 Source: Mathlib/RingTheory/RingHom/Locally.lean

Statistics

Metric	Count
Definitions Locally	1
Theorems locally_StableUnderCompositionWithLocalizationAwaySource, locally_StableUnderCompositionWithLocalizationAwayTarget, locally_holdsForLocalizationAway, locally_iff_exists, locally_iff_finite, locally_iff_isLocalization, locally_iff_of_localizationSpanTarget, locally_isStableUnderBaseChange, locally_localizationAwayPreserves, locally_localizationPreserves, locally_of, locally_ofLocalizationSpanTarget, locally_of_exists, locally_of_locally, locally_propertyIsLocal, locally_respectsIso, locally_stableUnderComposition	17
Total	18

RingHom

Definitions

Name	Category	Theorems
Locally 📖	MathDef	20 math math: locally_iff_of_localizationSpanTarget, locally_iff_isLocalization, AlgebraicGeometry.instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension, locally_isStableUnderBaseChange, locally_StableUnderCompositionWithLocalizationAwayTarget, locally_localizationAwayPreserves, locally_holdsForLocalizationAway, locally_of_exists, locally_ofLocalizationSpanTarget, locally_localizationPreserves, smooth_iff_locally_isStandardSmooth, AlgebraicGeometry.HasRingHomProperty.locally_of_iff, locally_StableUnderCompositionWithLocalizationAwaySource, locally_of, locally_iff_finite, Smooth.locally_isStandardSmooth, locally_iff_exists, locally_propertyIsLocal, locally_stableUnderComposition, locally_respectsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locally_StableUnderCompositionWithLocalizationAwaySource 📖	mathematical	StableUnderCompositionWithLocalizationAwaySource	Locally	—	comp_assoc
locally_StableUnderCompositionWithLocalizationAwayTarget 📖	mathematical	StableUnderCompositionWithLocalizationAwayTarget	Locally	—	Ideal.map_span instRingHomClass Ideal.map_top Localization.isLocalization IsLocalization.map_comp comp_assoc IsLocalization.Away.commutes IsScalarTower.of_algebraMap_eq IsLocalization.map_eq OreLocalization.instIsScalarTower IsScalarTower.right
locally_holdsForLocalizationAway 📖	mathematical	HoldsForLocalizationAway	Locally	—	Ideal.span_singleton_one IsScalarTower.right OreLocalization.instIsScalarTower Localization.isLocalization Submonoid.powers_one IsScalarTower.algebraMap_eq IsLocalization.isLocalization_of_algEquiv
locally_iff_exists 📖	mathematical	RespectsIso	Locally comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring algebraMap	—	Subtype.range_coe_subtype Localization.isLocalization locally_of_exists
locally_iff_finite 📖	mathematical	—	Locally Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing algebraMap OreLocalization.instAlgebra Algebra.id	—	Ideal.span_eq_top_iff_finite
locally_iff_isLocalization 📖	mathematical	RespectsIso	Locally comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring algebraMap	—	locally_iff_finite Localization.isLocalization ext AlgEquiv.commutes comp_assoc
locally_iff_of_localizationSpanTarget 📖	mathematical	RespectsIso OfLocalizationSpanTarget	Locally	—	locally_of
locally_isStableUnderBaseChange 📖	mathematical	RespectsIso IsStableUnderBaseChange	Locally	—	locally_respectsIso Algebra.to_smulCommClass locally_iff_exists Set.image_eq_range Ideal.map_span AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.map_top IsScalarTower.right IsScalarTower.to_smulCommClass IsScalarTower.left OreLocalization.instIsScalarTower Submonoid.map_powers IsScalarTower.of_algebraMap_eq' isLocalizedModule_iff_isLocalization isLocalizedModule_iff_isBaseChange Localization.isLocalization Algebra.IsPushout.out TensorProduct.isScalarTower_left Algebra.TensorProduct.right_isScalarTower Algebra.IsPushout.comp_iff IsScalarTower.of_algHom IsScalarTower.of_algebraMap_eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass TensorProduct.isPushout' IsScalarTower.algebraMap_eq
locally_localizationAwayPreserves 📖	mathematical	LocalizationAwayPreserves	Locally	—	locally_iff_exists LocalizationAwayPreserves.respectsIso MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass Set.image_eq_range Ideal.map_span Ideal.map_top Localization.isLocalization Submonoid.map_powers IsLocalization.commutes IsScalarTower.of_algebraMap_eq' IsLocalization.map_comp OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.Away.instMapRingHomPowersOfCoe Submonoid.map.congr_simp algebraMap_toAlgebra IsLocalization.Away.map.eq_1 IsLocalization.map_comp_map
locally_localizationPreserves 📖	mathematical	LocalizationPreserves	Locally	—	locally_iff_exists LocalizationAwayPreserves.respectsIso LocalizationPreserves.away MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass MonoidHom.instMonoidHomClass Submonoid.map_map Set.image_eq_range Ideal.map_span Ideal.map_top Localization.isLocalization Submonoid.le_comap_map Submonoid.map_powers IsLocalization.commutes IsScalarTower.of_algebraMap_eq' IsLocalization.map_comp OreLocalization.instIsScalarTower IsScalarTower.right algebraMap_toAlgebra IsLocalization.map_comp_map
locally_of 📖	mathematical	RespectsIso	Locally	—	Localization.isLocalization Submonoid.powers_one Ideal.span_singleton_one
locally_ofLocalizationSpanTarget 📖	mathematical	RespectsIso	OfLocalizationSpanTarget Locally	—	locally_iff_exists Localization.isLocalization IsLocalization.Away.span_range_mulNumerator_eq_top IsLocalization.Away.mul' OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.Away.of_associated IsLocalization.Away.sec_spec associated_mul_unit_right map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass IsUnit.pow IsLocalization.Away.algebraMap_isUnit IsScalarTower.algebraMap_eq
locally_of_exists 📖	mathematical	RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set.range Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalization.Away comp algebraMap	Locally	—	Localization.isLocalization ext AlgEquiv.commutes comp_assoc
locally_of_locally 📖	—	Locally	—	—	—
locally_propertyIsLocal 📖	mathematical	LocalizationAwayPreserves StableUnderCompositionWithLocalizationAway	PropertyIsLocal Locally	—	locally_localizationAwayPreserves locally_ofLocalizationSpanTarget LocalizationAwayPreserves.respectsIso OfLocalizationSpanTarget.ofLocalizationSpan locally_StableUnderCompositionWithLocalizationAwaySource locally_StableUnderCompositionWithLocalizationAwayTarget
locally_respectsIso 📖	mathematical	RespectsIso	Locally	—	Ideal.map_span RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Ideal.map_top Localization.isLocalization Submonoid.map_powers MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass ext IsLocalization.map_eq comp_assoc
locally_stableUnderComposition 📖	mathematical	RespectsIso LocalizationPreserves StableUnderComposition	Locally	—	locally_iff_finite locally_iff_exists eq_top_iff Ideal.span_le Subtype.range_coe_subtype Finset.sum_congr Pi.single_apply mul_ite mul_one MulZeroClass.mul_zero ite_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass instRingHomClass MulZeroClass.zero_mul Fintype.sum_prod_type Finset.sum_ite_eq' RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass one_mul IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap Localization.isLocalization ext IsLocalization.map_eq IsLocalization.Away.instMapRingHomPowersOfCoe

---

← Back to Index