Loogle!

Result

Found 21 declarations mentioning AlgebraicGeometry.Scheme.IdealSheafData.map.

• AlgebraicGeometry.Scheme.IdealSheafData.map 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) : Y.IdealSheafData
• AlgebraicGeometry.Scheme.IdealSheafData.map_id 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {Z : AlgebraicGeometry.Scheme} (I : Z.IdealSheafData) : I.map (CategoryTheory.CategoryStruct.id Z) = I
• AlgebraicGeometry.Scheme.IdealSheafData.map_mono 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Monotone fun x => x.map f
• AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) : (I.map f).comap f ≤ I
• AlgebraicGeometry.Scheme.IdealSheafData.le_map_comap 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (J : Y.IdealSheafData) (f : X ⟶ Y) : J ≤ (J.comap f).map f
• AlgebraicGeometry.Scheme.IdealSheafData.map_bot 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : ⊥.map f = AlgebraicGeometry.Scheme.Hom.ker f
• AlgebraicGeometry.Scheme.IdealSheafData.map_gc 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : GaloisConnection (fun x => x.comap f) fun x => x.map f
• AlgebraicGeometry.Scheme.IdealSheafData.map.eq_1 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) : I.map f = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp I.subschemeι f)
• AlgebraicGeometry.Scheme.Hom.ker_comp 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g) = (AlgebraicGeometry.Scheme.Hom.ker f).map g
• AlgebraicGeometry.Scheme.IdealSheafData.map_ker 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (AlgebraicGeometry.Scheme.Hom.ker f).map g = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g)
• AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) : I.subscheme ⟶ J.subscheme
• AlgebraicGeometry.Scheme.IdealSheafData.map_comp 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y Z : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z) : I.map (CategoryTheory.CategoryStruct.comp f g) = (I.map f).map g
• AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {f : X ⟶ Y} {J : Y.IdealSheafData} : J ≤ I.map f ↔ J.comap f ≤ I
• AlgebraicGeometry.Scheme.IdealSheafData.map_inf 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I₁ I₂ : X.IdealSheafData) (f : X ⟶ Y) : (I₁ ⊓ I₂).map f = I₁.map f ⊓ I₂.map f
• AlgebraicGeometry.Scheme.IdealSheafData.map_top 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : ⊤.map f = ⊤
• AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) : CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) J.subschemeι = CategoryTheory.CategoryStruct.comp I.subschemeι f
• AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι_assoc 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) (CategoryTheory.CategoryStruct.comp J.subschemeι h) = CategoryTheory.CategoryStruct.comp I.subschemeι (CategoryTheory.CategoryStruct.comp f h)
• AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (Z : TopologicalSpace.Closeds ↥X) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z).map f = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' ↑Z))
• AlgebraicGeometry.Scheme.IdealSheafData.support_map 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] : (I.map f).support = TopologicalSpace.Closeds.closure (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' ↑I.support)
• AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (U : ↑Y.affineOpens) : (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U)) (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, ⋯⟩)
• AlgebraicGeometry.Scheme.IdealSheafData.ideal_map 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (U : ↑Y.affineOpens) (H : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj ↑U)) : (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U)) (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, H⟩)

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 ff04530 serving mathlib revision 8623f65