[GOAL]
X Y Z : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U
[PROOFSTEP]
simp
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).toPrefunctor.obj ∘ U)
[PROOFSTEP]
ext1
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).toPrefunctor.obj ∘ U))
[PROOFSTEP]
rw [iSup_def, iSup_def, map_obj]
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := ↑f ⁻¹' ⋃ (i : ι), ↑(U i), is_open' := (_ : IsOpen (↑f ⁻¹' ⋃ (i : ι), ↑(U i))) } =
    ↑{ carrier := ⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i),
        is_open' := (_ : IsOpen (⋃ (i : ι), ↑(((map f).toPrefunctor.obj ∘ U) i))) }
[PROOFSTEP]
dsimp
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑f ⁻¹' ⋃ (i : ι), ↑(U i) = ⋃ (i : ι), ↑((map f).obj (U i))
[PROOFSTEP]
rw [Set.preimage_iUnion]
[GOAL]
case h
X Y Z : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ⋃ (i : ι), ↑f ⁻¹' ↑(U i) = ⋃ (i : ι), ↑((map f).obj (U i))
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U
[PROOFSTEP]
rw [congr_arg map h]
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
⊢ map f = map g
[PROOFSTEP]
subst h
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
⊢ map f = map f
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U
[PROOFSTEP]
rw [h]
[GOAL]
X Y Z : TopCat
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map g).obj U = (map f).obj U
[PROOFSTEP]
rw [h]
[GOAL]
X✝ Y✝ Z X Y : TopCat
H : X ≅ Y
U : Opens ↑Y
⊢ (𝟭 (Opens ↑Y)).obj U = (map H.hom ⋙ map H.inv).obj U
[PROOFSTEP]
simp [map, Set.preimage_preimage]
[GOAL]
X✝ Y✝ Z X Y : TopCat
H : X ≅ Y
U : Opens ↑X
⊢ (map H.inv ⋙ map H.hom).obj U = (𝟭 (Opens ↑X)).obj U
[PROOFSTEP]
simp [map, Set.preimage_preimage]
[GOAL]
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
H : Mono f
X✝ Y✝ : Opens ↑X
i : (functor hf).obj X✝ ⟶ (functor hf).obj Y✝
x : ↑X
hx : x ∈ ↑X✝
⊢ x ∈ ↑Y✝
[PROOFSTEP]
obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
H : Mono f
X✝ Y✝ : Opens ↑X
i : (functor hf).obj X✝ ⟶ (functor hf).obj Y✝
x : ↑X
hx : x ∈ ↑X✝
y : (forget TopCat).obj X
hy : y ∈ ↑Y✝
eq : ↑f y = ↑f x
⊢ x ∈ ↑Y✝
[PROOFSTEP]
exact (TopCat.mono_iff_injective f).mp H eq ▸ hy
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ⊤ = U
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ⊤) = ↑U
[PROOFSTEP]
exact Set.image_univ.trans Subtype.range_coe
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (map (inclusion U)).obj U = ⊤
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U : Opens ↑X
⊢ ↑((map (inclusion U)).obj U) = ↑⊤
[PROOFSTEP]
exact Subtype.coe_preimage_self _
[GOAL]
X : TopCat
U : Opens ↑X
⊢ (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj U = (𝟭 (Opens ↑X)).obj U
[PROOFSTEP]
simp
[GOAL]
X : TopCat
⊢ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤)) = map (inclusionTopIso X).inv
[PROOFSTEP]
refine' CategoryTheory.Functor.ext _ _
[GOAL]
case refine'_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)),
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj X_1 = (map (inclusionTopIso X).inv).obj X_1
[PROOFSTEP]
intro U
[GOAL]
case refine'_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U = (map (inclusionTopIso X).inv).obj U
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.h.h
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U) ↔ x ∈ ↑((map (inclusionTopIso X).inv).obj U)
[PROOFSTEP]
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
[GOAL]
case refine'_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).map f =
      eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj X_1 = (map (inclusionTopIso X).inv).obj X_1) ≫
        (map (inclusionTopIso X).inv).map f ≫
          eqToHom (_ : (map (inclusionTopIso X).inv).obj Y = (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj Y)
[PROOFSTEP]
intros U V f
[GOAL]
case refine'_2
X : TopCat
U V : Opens ↑((toTopCat X).obj ⊤)
f : U ⟶ V
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).map f =
    eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj U = (map (inclusionTopIso X).inv).obj U) ≫
      (map (inclusionTopIso X).inv).map f ≫
        eqToHom (_ : (map (inclusionTopIso X).inv).obj V = (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion ⊤))).obj V)
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
⊢ (IsOpenMap.functor hf).obj ((map f).obj U) = (IsOpenMap.functor hf).obj ⊤ ⊓ U
[PROOFSTEP]
ext
[GOAL]
case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) ↔ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
constructor
[GOAL]
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x : (forget TopCat).obj X
hx : x ∈ ↑((map f).obj U)
⊢ ↑f x ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
[PROOFSTEP]
exact ⟨⟨x, trivial, rfl⟩, hx⟩
[GOAL]
case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
[PROOFSTEP]
rintro ⟨⟨x, -, rfl⟩, hx⟩
[GOAL]
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ↑f
U : Opens ↑Y
x : (forget TopCat).obj X
hx : ↑f x ∈ ↑U
⊢ ↑f x ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
X : TopCat
U : Opens ↑X
⊢ Set.range ((forget TopCat).map (inclusion U)) = ↑U
[PROOFSTEP]
ext x
[GOAL]
case h
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U)) ↔ x ∈ ↑U
[PROOFSTEP]
constructor
[GOAL]
case h.mp
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U)) → x ∈ ↑U
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case h.mp.intro
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj ((toTopCat X).obj U)
⊢ (forget TopCat).map (inclusion U) x ∈ ↑U
[PROOFSTEP]
exact x.2
[GOAL]
case h.mpr
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
⊢ x ∈ ↑U → x ∈ Set.range ((forget TopCat).map (inclusion U))
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
X : TopCat
U : Opens ↑X
x : (forget TopCat).obj X
h : x ∈ ↑U
⊢ x ∈ Set.range ((forget TopCat).map (inclusion U))
[PROOFSTEP]
exact ⟨⟨x, h⟩, rfl⟩
[GOAL]
X : TopCat
U V : Opens ↑X
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ((map (inclusion U)).obj V) = V ⊓ U
[PROOFSTEP]
ext1
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ ↑((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj ((map (inclusion U)).obj V)) = ↑(V ⊓ U)
[PROOFSTEP]
refine' Set.image_preimage_eq_inter_range.trans _
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ (V.1 ∩ Set.range fun x => ↑(inclusion U) x) = ↑(V ⊓ U)
[PROOFSTEP]
erw [set_range_forget_map_inclusion U]
[GOAL]
case h
X : TopCat
U V : Opens ↑X
⊢ V.1 ∩ ↑U = ↑(V ⊓ U)
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
      ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
    (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V)
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
      ((map (inclusion U)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V)) =
    (IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V
[PROOFSTEP]
rw [map_functor_eq V]
[GOAL]
X : TopCat
U : Opens ↑X
V : Opens { x // x ∈ U }
⊢ NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑(inclusion U))).counit
      ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
    eqToHom
      (_ :
        (map (inclusion U) ⋙ IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj
            ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V) =
          (𝟭 (Opens ↑X)).obj ((IsOpenMap.functor (_ : IsOpenMap ↑(inclusion U))).obj V))
[PROOFSTEP]
apply Subsingleton.elim
