Away

📁 Source: Mathlib/GroupTheory/MonoidLocalization/Away.lean

Statistics

Metric	Count
Definitions Away, addEquivOfQuotient, addMonoidOf, negSelf, AwayMap, negSelf, awayToAwayRight, Away, Away, Away, Away, invSelf, monoidOf, mulEquivOfQuotient, AwayMap, invSelf, awayToAwayRight	17
Theorems mk_eq_addMonoidOf_mk', lift_comp, lift_eq, mk_eq_monoidOf_mk', lift_comp, lift_eq	6
Total	23

AddLocalization

Definitions

Name	Category	Theorems
Away 📖	CompOp	1 math math: Away.mk_eq_addMonoidOf_mk'

AddLocalization.Away

Definitions

Name	Category	Theorems
addEquivOfQuotient 📖	CompOp	—
addMonoidOf 📖	CompOp	1 math math: mk_eq_addMonoidOf_mk'
negSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_addMonoidOf_mk' 📖	mathematical	—	AddSubmonoid.multiples AddCommMonoid.toAddMonoid AddSubmonoid.LocalizationMap.mk' AddLocalization.Away AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm addMonoidOf	—	AddLocalization.mk_eq_addMonoidOf_mk'

AddSubmonoid.LocalizationMap

Definitions

Name	Category	Theorems
AwayMap 📖	CompOp	2 math math: AwayMap.lift_comp, AwayMap.lift_eq
awayToAwayRight 📖	CompOp	—

AddSubmonoid.LocalizationMap.AwayMap

Definitions

Name	Category	Theorems
negSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_comp 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	AddMonoidHom.comp lift AddMonoidHomClass.toAddMonoidHom AddSubmonoid.LocalizationMap.AwayMap AddSubmonoid.LocalizationMap.instFunLike AddSubmonoid.multiples AddSubmonoid.LocalizationMap.instAddMonoidHomClass	—	AddSubmonoid.LocalizationMap.lift_comp
lift_eq 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	lift AddSubmonoid.LocalizationMap.AwayMap AddSubmonoid.LocalizationMap.instFunLike AddSubmonoid.multiples	—	AddSubmonoid.LocalizationMap.lift_eq

HomogeneousLocalization

Definitions

Name	Category	Theorems
Away 📖	CompOp	72 math math: AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, range_awayMapAux_subset, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Away.adjoin_mk_prod_pow_eq_top, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, awayMap_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, val_awayMap, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, awayMapₐ_apply, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, awayMap_fromZeroRingHom, Away.span_mk_prod_pow_eq_top, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Proj.opensRange_awayι, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, Away.isLocalization_mul, val_awayMap_eq_aux, val_awayMap_mk, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, awayMapAux_mk, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun_asIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.instIsOpenImmersionAwayι, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Away.finiteType, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective

IsLocalization

Definitions

Name	Category	Theorems
Away 📖	MathDef	38 math math: AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton, Away.mul, AlgebraicGeometry.Γ_restrict_isLocalization, Away.tensorRight, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, Away.mul_of_isUnit', Away.commutes, Away.of_surjective_of_isScalarTower, away_of_isUnit_of_bijective, away_snd, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway, Away.mul_of_associated, away_of_isIdempotentElem_of_mul, Algebra.IsStandardOpenImmersion.exists_away, away_of_isIdempotentElem, Away.quotient_of_isIdempotentElem, Away.mul', Away.mk, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, Away.instHMulAwayCoeRingHomAlgebraMap, Away.instHMulAwayCoeRingHomAlgebraMap_1, AlgebraicGeometry.isLocalization_away_of_isAffine, Away.tensor, HomogeneousLocalization.Away.isLocalization_mul, Algebra.isStandardOpenImmersion_iff, Away.of_surjective, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, adjoin_inv, away_fst, LaurentPolynomial.isLocalization, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, Away.iff_of_associated, Away.integralClosure, AlgebraicGeometry.isLocalization_basicOpen_of_qcqs, Away.of_associated, Away.mul_of_isUnit

IsLocalizedModule

Definitions

Name	Category	Theorems
Away 📖	MathDef	—

Localization

Definitions

Name	Category	Theorems
Away 📖	CompOp	56 math math: Algebra.exists_unramified_of_isUnramifiedAt, Away.mk_eq_monoidOf_mk', HasStandardEtaleSurjectionOn.isStandardEtale, algebraMap_injective_of_span_eq_top, Algebra.basicOpen_subset_etaleLocus_iff_etale, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, AlgebraicGeometry.Scheme.basic_open_isOpenImmersion, HomogeneousLocalization.range_awayMapAux_subset, Module.basicOpen_subset_freeLocus_iff, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.basicOpen_subset_unramifiedLocus_iff, instFinitePresentationAway, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, HomogeneousLocalization.val_awayMap, awayMap_surjective_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', Algebra.basicOpen_subset_smoothLocus_iff_smooth, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_X_carrier, Algebra.basicOpen_subset_etaleLocus_iff, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, Algebra.IsSmoothAt.exists_notMem_smooth, exists_awayMap_bijective_of_residueField_surjective, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Algebra.IsEtaleAt.exists_isStandardEtale, exists_awayMap_injective_of_localRingHom_injective, instFiniteTypeAway, Algebra.exists_formallyUnramified_of_isUnramifiedAt, localization_unit_isIso, HomogeneousLocalization.val_awayMap_eq_aux, HomogeneousLocalization.awayMapAux_mk, Algebra.exists_etale_of_isEtaleAt, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, Surreal.dyadicMap_apply, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, RingHom.RespectsIso.isLocalization_away_iff, awayMap_injective_iff, RingHom.locally_iff_finite, localization_unit_isIso', IsLocalization.ideal_eq_iInf_comap_map_away, exists_awayMap_bijective_of_localRingHom_bijective, Algebra.basicOpen_subset_smoothLocus_iff, awayLift_mk, Surreal.dyadicMap_apply_pow, Algebra.Etale.instAway, Algebra.instIsStandardOpenImmersionAway, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective

Localization.Away

Definitions

Name	Category	Theorems
invSelf 📖	CompOp	—
monoidOf 📖	CompOp	1 math math: mk_eq_monoidOf_mk'
mulEquivOfQuotient 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_monoidOf_mk' 📖	mathematical	—	Submonoid.powers CommMonoid.toMonoid Submonoid.LocalizationMap.mk' Localization.Away OreLocalization.instCommMonoid OreLocalization.oreSetComm monoidOf	—	Localization.mk_eq_monoidOf_mk'

Submonoid.LocalizationMap

Definitions

Name	Category	Theorems
AwayMap 📖	CompOp	2 math math: AwayMap.lift_comp, AwayMap.lift_eq
awayToAwayRight 📖	CompOp	—

Submonoid.LocalizationMap.AwayMap

Definitions

Name	Category	Theorems
invSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_comp 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	MonoidHom.comp lift MonoidHomClass.toMonoidHom Submonoid.LocalizationMap.AwayMap Submonoid.LocalizationMap.instFunLike Submonoid.powers Submonoid.LocalizationMap.instMonoidHomClass	—	Submonoid.LocalizationMap.lift_comp
lift_eq 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	lift Submonoid.LocalizationMap.AwayMap Submonoid.LocalizationMap.instFunLike Submonoid.powers	—	Submonoid.LocalizationMap.lift_eq

---

← Back to Index