case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Mono f → Function.Injective ((forget CompHaus).map f)

case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Injective ((forget CompHaus).map f) → Mono f
X Y : CompHaus
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ((forget CompHaus).map f)
constructor
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Mono f → Function.Injective ((forget CompHaus).map f)
intro hf x₁ x₂ h
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
⊢ x₁ = x₂
let g₁ : of PUnit ⟶ X := ⟨fun _ => x₁, continuous_const⟩
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
⊢ x₁ = x₂
let g₂ : of PUnit ⟶ X := ⟨fun _ => x₂, continuous_const⟩
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
⊢ x₁ = x₂
have : g₁ ≫ f = g₂ ≫ f := by
  ext
  exact h
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ = g₂
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂
rw [cancel_mono] at this
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : (forget CompHaus).map g₁ PUnit.unit = (forget CompHaus).map g₂ PUnit.unit
⊢ x₁ = x₂
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : g₁ = g₂
⊢ x₁ = x₂
apply_fun fun e => e PUnit.unit  at this
no goals
case mp
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
this : (forget CompHaus).map g₁ PUnit.unit = (forget CompHaus).map g₂ PUnit.unit
⊢ x₁ = x₂
exact this
case w
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
x✝ : (forget CompHaus).obj (of PUnit)
⊢ (forget CompHaus).map (g₁ ≫ f) x✝ = (forget CompHaus).map (g₂ ≫ f) x✝
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
⊢ g₁ ≫ f = g₂ ≫ f
ext
no goals
case w
X Y : CompHaus
f : X ⟶ Y
hf : Mono f
x₁ x₂ : (forget CompHaus).obj X
h : (forget CompHaus).map f x₁ = (forget CompHaus).map f x₂
g₁ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₁
g₂ : of PUnit ⟶ X := ContinuousMap.mk fun x => x₂
x✝ : (forget CompHaus).obj (of PUnit)
⊢ (forget CompHaus).map (g₁ ≫ f) x✝ = (forget CompHaus).map (g₂ ≫ f) x✝
exact h
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Mono ((forget CompHaus).map f) → Mono f
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Injective ((forget CompHaus).map f) → Mono f
rw [← CategoryTheory.mono_iff_injective]
no goals
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Mono ((forget CompHaus).map f) → Mono f
apply (forget CompHaus).mono_of_mono_map