feat(topology/*): Gluing topological spaces (#9864)

Co-authored-by: erdOne <[email protected]>
Co-authored-by: Adam Topaz <[email protected]>

Author: erdOne

src/algebraic_geometry/properties.lean

@@ -123,8 +123,6 @@ begin
     ((as_iso $ to_Spec_Γ R).CommRing_iso_to_ring_equiv.injective)
 end
 
-local attribute [elementwise] category_theory.is_iso.hom_inv_id
-
 lemma basic_open_eq_of_affine {R : CommRing} (f : R) :
   RingedSpace.basic_open (Spec.to_SheafedSpace.obj (op R)) ((Spec_Γ_identity.app R).inv f) =
     prime_spectrum.basic_open f :=

src/category_theory/concrete_category/elementwise.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import tactic.elementwise
+import category_theory.limits.has_limits
+import category_theory.limits.shapes.kernels
+
+/-!
+In this file we provide various simp lemmas in its elementwise form via `tactic.elementwise`.
+-/
+
+open category_theory category_theory.limits
+
+attribute [elementwise]
+  cone.w limit.lift_π limit.w cocone.w colimit.ι_desc colimit.w
+  kernel.condition cokernel.condition
+  -- Note that the elementwise forms of `iso.hom_inv_id` and `iso.inv_hom_id` are already
+  -- provided as `category_theory.coe_hom_inv_id` and `category_theory.coe_inv_hom_id`.
+  is_iso.hom_inv_id is_iso.inv_hom_id

src/category_theory/limits/concrete_category.lean

@@ -7,7 +7,7 @@ import category_theory.limits.preserves.basic
 import category_theory.limits.types
 import category_theory.limits.shapes.wide_pullbacks
 import category_theory.limits.shapes.multiequalizer
-import tactic.elementwise
+import category_theory.concrete_category.elementwise
 
 /-!
 # Facts about (co)limits of functors into concrete categories
@@ -19,8 +19,6 @@ open category_theory
 
 namespace category_theory.limits
 
-attribute [elementwise] cone.w limit.lift_π limit.w cocone.w colimit.ι_desc colimit.w
-
 local attribute [instance] concrete_category.has_coe_to_fun concrete_category.has_coe_to_sort
 
 section limits

src/category_theory/limits/shapes/concrete_category.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import category_theory.limits.shapes.kernels
 import category_theory.concrete_category.basic
-import tactic.elementwise
+import category_theory.concrete_category.elementwise
 
 /-!
 # Facts about limits of functors into concrete categories
@@ -18,10 +18,3 @@ while comparing categorical limits with existing constructions in concrete categ
 universes u
 
 open category_theory
-
-
-namespace category_theory.limits
-
-attribute [elementwise] kernel.condition cokernel.condition
-
-end category_theory.limits

src/logic/function/basic.lean

@@ -751,3 +751,7 @@ def set.separates_points {α β : Type*} (A : set (α → β)) : Prop :=
 
 lemma is_symm_op.flip_eq {α β} (op) [is_symm_op α β op] : flip op = op :=
 funext $ λ a, funext $ λ b, (is_symm_op.symm_op a b).symm
+
+lemma inv_image.equivalence {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β)
+  (h : equivalence r) : equivalence (inv_image r f) :=
+⟨λ _, h.1 _, λ _ _ x, h.2.1 x, inv_image.trans r f h.2.2⟩