Loogle!

Result

Found 12 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)
• RingHom.RespectsIso.is_localization_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.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
• 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
• 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)
• 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.toPrefunctor.1 (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.toPrefunctor.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)
• RingHom.localization_away_map_finite 📋 Mathlib.RingTheory.RingHom.Finite
  {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (R' S' : Type u) [CommRing R'] [CommRing S'] [Algebra R R'] [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 : Type u} [CommRing R] [CommRing S] (f : R →+* S) (R' S' : Type u) [CommRing R'] [CommRing S'] [Algebra R R'] [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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 19971e9 serving mathlib revision bce1d65