[GOAL]
R : TopCommRingCat
⊢ Continuous ↑(RingHom.id R.α)
[PROOFSTEP]
rw [RingHom.id]
[GOAL]
R : TopCommRingCat
⊢ Continuous
    ↑{
        toMonoidHom :=
          { toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
            map_mul' :=
              (_ :
                ∀ (x y : R.α),
                  OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                    OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) },
        map_zero' :=
          (_ :
            OneHom.toFun
                (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : R.α),
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                0 =
              OneHom.toFun
                (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : R.α),
                          OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                0),
        map_add' :=
          (_ :
            ∀ (x y : R.α),
              OneHom.toFun
                  (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                      map_mul' :=
                        (_ :
                          ∀ (x y : R.α),
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                              OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                  (x + y) =
                OneHom.toFun
                  (↑{ toOneHom := { toFun := id, map_one' := (_ : id 1 = id 1) },
                      map_mul' :=
                        (_ :
                          ∀ (x y : R.α),
                            OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y) =
                              OneHom.toFun { toFun := id, map_one' := (_ : id 1 = id 1) } (x * y)) })
                  (x + y)) }
[PROOFSTEP]
continuity
[GOAL]
X✝ Y✝ Z✝ : TopCommRingCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Continuous ↑(RingHom.comp ↑g ↑f)
[PROOFSTEP]
cases f
[GOAL]
case mk
X✝ Y✝ Z✝ : TopCommRingCat
g : Y✝ ⟶ Z✝
val✝ : X✝.α →+* Y✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑(RingHom.comp ↑g ↑{ val := val✝, property := property✝ })
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑(RingHom.comp ↑{ val := val✝, property := property✝ } ↑{ val := val✝¹, property := property✝¹ })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous (↑val✝ ∘ ↑val✝¹)
[PROOFSTEP]
apply Continuous.comp
[GOAL]
case mk.mk.hg
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑val✝
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.hf
X✝ Y✝ Z✝ : TopCommRingCat
val✝¹ : X✝.α →+* Y✝.α
property✝¹ : Continuous ↑val✝¹
val✝ : Y✝.α →+* Z✝.α
property✝ : Continuous ↑val✝
⊢ Continuous ↑val✝¹
[PROOFSTEP]
assumption
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i_Top :=
  asIso
    ((forget₂ TopCommRingCat TopCat).map f)
      -- and a `RingEquiv`.
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e_Ring : X ≃+* Y :=
  { f.1, ((forget TopCat).mapIso i_Top).toEquiv with }
    -- Putting these together we obtain the isomorphism we're after:
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ IsIso f
[PROOFSTEP]
exact
  ⟨⟨⟨e_Ring.symm, i_Top.inv.2⟩,
      ⟨by
        ext x
        exact e_Ring.left_inv x, by
        ext x
        exact e_Ring.right_inv x⟩⟩⟩
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ f ≫ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } = 𝟙 X
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
x : (forget TopCommRingCat).obj X
⊢ ↑(f ≫ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) }) x = ↑(𝟙 X) x
[PROOFSTEP]
exact e_Ring.left_inv x
[GOAL]
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
⊢ { val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } ≫ f = 𝟙 Y
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let src := ↑f;
  let src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  {
    toEquiv :=
      { toFun := src.toFun, invFun := src_1.invFun, left_inv := (_ : Function.LeftInverse src_1.invFun src_1.toFun),
        right_inv := (_ : Function.RightInverse src_1.invFun src_1.toFun) },
    map_mul' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x * y) = OneHom.toFun (↑↑src) x * OneHom.toFun (↑↑src) y),
    map_add' := (_ : ∀ (x y : X.α), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) }
x : (forget TopCommRingCat).obj Y
⊢ ↑({ val := ↑(RingEquiv.symm e_Ring), property := (_ : Continuous i_Top.inv.toFun) } ≫ f) x = ↑(𝟙 Y) x
[PROOFSTEP]
exact e_Ring.right_inv x
