Loogle!

Result

Found 15 declarations mentioning IsLocalization.Away.map.

IsLocalization.Away.map 📋 Mathlib.RingTheory.Localization.Away.Basic
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (f : R →+* P) (r : R) [IsLocalization.Away r S] [IsLocalization.Away (f r) Q] : S →+* Q
IsLocalization.Away.mapₐ_apply 📋 Mathlib.RingTheory.Localization.Away.Basic
{R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [IsLocalization.Away a Aₚ] [IsLocalization.Away (f a) Bₚ] (x : Aₚ) : (IsLocalization.Away.mapₐ Aₚ Bₚ f a) x = (IsLocalization.Away.map Aₚ Bₚ f.toRingHom a) x
RingHom.RespectsIso.isLocalization_away_iff 📋 Mathlib.RingTheory.RingHomProperties
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso P) {R S : Type u} (R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] : P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
IsLocalization.Away.map.congr_simp 📋 Mathlib.RingTheory.LocalProperties.Exactness
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (f f✝ : R →+* P) (e_f : f = f✝) (r r✝ : R) (e_r : r = r✝) [IsLocalization.Away r S] [IsLocalization.Away (f r) Q] : IsLocalization.Away.map S Q f r = IsLocalization.Away.map S Q f✝ r✝
bijective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
{R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Bijective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Bijective ⇑f
injective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
{R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Injective ⇑f
surjective_of_isLocalization_of_span_eq_top 📋 Mathlib.RingTheory.LocalProperties.Exactness
{R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {s : Set R} (hs : Ideal.span s = ⊤) (Rᵣ : ↑s → Type u_3) [(r : ↑s) → CommSemiring (Rᵣ r)] [(r : ↑s) → Algebra R (Rᵣ r)] (Sᵣ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Sᵣ r)] [(r : ↑s) → Algebra S (Sᵣ r)] (f : R →+* S) [∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)] [∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)] (h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)) : Function.Surjective ⇑f
IsLocalization.Away.map.eq_1 📋 Mathlib.RingTheory.LocalProperties.Basic
{R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (f : R →+* P) (r : R) [IsLocalization.Away r S] [IsLocalization.Away (f r) Q] : IsLocalization.Away.map S Q f r = IsLocalization.map Q f ⋯
RingHom.OfLocalizationSpan.ofIsLocalization' 📋 Mathlib.RingTheory.LocalProperties.Basic
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P) (hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤) (hT : ∀ (r : ↑s), ∃ Rᵣ Sᵣ x x_1 x_2 x_3, ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ), P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)) : P f
AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (r : ↑(Y.presheaf.obj (Opposite.op U))) : AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)) ⋯ = CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.1 (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.1 (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r))))) (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)) r)
AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMap 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (h : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) (r : ↑(Y.presheaf.obj (Opposite.op U))) : CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.app f (Y.basicOpen r)) ≅ CategoryTheory.Arrow.mk (CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r))))) (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r))
AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map 📋 Mathlib.AlgebraicGeometry.AffineScheme
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (h : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) (r : ↑(Y.presheaf.obj (Opposite.op U))) : AlgebraicGeometry.Scheme.Hom.app f (Y.basicOpen r) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r))))) (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)
Localization.awayMap.eq_1 📋 Mathlib.RingTheory.RingHom.Surjective
{R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) : Localization.awayMap f r = IsLocalization.Away.map (Localization.Away r) (Localization.Away (f r)) f r
RingHom.localization_away_map_finite 📋 Mathlib.RingTheory.RingHom.Finite
(R S R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] (f : R →+* S) [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.Finite) : (IsLocalization.Away.map R' S' f r).Finite
RingHom.localization_away_map_finiteType 📋 Mathlib.RingTheory.RingHom.FiniteType
(R S R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R'] (f : R →+* S) [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : f.FiniteType) : (IsLocalization.Away.map R' S' f r).FiniteType

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision edaf32c