[GOAL]
X : Profinite
⊢ TopologicalSpace ((forget Profinite).obj X)
[PROOFSTEP]
change TopologicalSpace X
[GOAL]
X : Profinite
⊢ TopologicalSpace ↑X.toCompHaus.toTop
[PROOFSTEP]
exact inferInstance
[GOAL]
X : Profinite
⊢ TotallyDisconnectedSpace ((forget Profinite).obj X)
[PROOFSTEP]
change TotallyDisconnectedSpace X
[GOAL]
X : Profinite
⊢ TotallyDisconnectedSpace ↑X.toCompHaus.toTop
[PROOFSTEP]
exact inferInstance
[GOAL]
X : Profinite
⊢ CompactSpace ((forget Profinite).obj X)
[PROOFSTEP]
change CompactSpace X
[GOAL]
X : Profinite
⊢ CompactSpace ↑X.toCompHaus.toTop
[PROOFSTEP]
exact inferInstance
[GOAL]
X : Profinite
⊢ T2Space ((forget Profinite).obj X)
[PROOFSTEP]
change T2Space X
[GOAL]
X : Profinite
⊢ T2Space ↑X.toCompHaus.toTop
[PROOFSTEP]
exact inferInstance
[GOAL]
X✝ Y✝ : FintypeCat
f : X✝ ⟶ Y✝
⊢ Continuous f
[PROOFSTEP]
continuity
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop
[PROOFSTEP]
change TotallyDisconnectedSpace ({u : ∀ j : J, F.obj j | _} : Type _)
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ TotallyDisconnectedSpace
    ↑{u | ∀ {i j : J} (f : i ⟶ j), ↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) (u i) = u j}
[PROOFSTEP]
exact Subtype.totallyDisconnectedSpace
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj (mk (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt)).map f ≫
        NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π Y =
      NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π X ≫ F.map f
[PROOFSTEP]
intro j k f
[GOAL]
J : Type u
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj (mk (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt)).map f ≫
      NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π k =
    NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π j ≫ F.map f
[PROOFSTEP]
ext ⟨g, p⟩
[GOAL]
case w.mk
J : Type u
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
f : j ⟶ k
g : (j : J) → ↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
p : g ∈ {u | ∀ {i j : J} (f : i ⟶ j), ↑(((F ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f) (u i) = u j}
⊢ ↑(((Functor.const J).obj (mk (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt)).map f ≫
          NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π k)
      { val := g, property := p } =
    ↑(NatTrans.app (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π j ≫ F.map f) { val := g, property := p }
[PROOFSTEP]
exact (p f).symm
[GOAL]
⊢ Limits.PreservesLimits (forget Profinite)
[PROOFSTEP]
apply Limits.compPreservesLimits Profinite.toTopCat (forget TopCat)
[GOAL]
X Y : Profinite
f : X ⟶ Y
⊢ ReflectsIsomorphisms (forget Profinite)
[PROOFSTEP]
constructor
[GOAL]
case reflects
X Y : Profinite
f : X ⟶ Y
⊢ ∀ {A B : Profinite} (f : A ⟶ B) [inst : IsIso ((forget Profinite).map f)], IsIso f
[PROOFSTEP]
intro A B f hf
[GOAL]
case reflects
X Y : Profinite
f✝ : X ⟶ Y
A B : Profinite
f : A ⟶ B
hf : IsIso ((forget Profinite).map f)
⊢ IsIso f
[PROOFSTEP]
exact Profinite.isIso_of_bijective _ ((isIso_iff_bijective f).mp hf)
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
⊢ ContinuousMap.mk ↑f ≫ ContinuousMap.mk ↑(Homeomorph.symm f) = 𝟙 X
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
x : (forget Profinite).obj X
⊢ ↑(ContinuousMap.mk ↑f ≫ ContinuousMap.mk ↑(Homeomorph.symm f)) x = ↑(𝟙 X) x
[PROOFSTEP]
exact f.symm_apply_apply x
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
⊢ ContinuousMap.mk ↑(Homeomorph.symm f) ≫ ContinuousMap.mk ↑f = 𝟙 Y
[PROOFSTEP]
ext x
[GOAL]
case w
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
x : (forget Profinite).obj Y
⊢ ↑(ContinuousMap.mk ↑(Homeomorph.symm f) ≫ ContinuousMap.mk ↑f) x = ↑(𝟙 Y) x
[PROOFSTEP]
exact f.apply_symm_apply x
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : X ≅ Y
x : ↑X.toCompHaus.toTop
⊢ ↑f.inv (↑f.hom x) = x
[PROOFSTEP]
simp
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : X ≅ Y
x : ↑Y.toCompHaus.toTop
⊢ ↑f.hom (↑f.inv x) = x
[PROOFSTEP]
simp
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w
X Y : Profinite
f✝ : X ⟶ Y
f : X ≅ Y
x✝ : (forget Profinite).obj X
⊢ ↑(isoOfHomeo (homeoOfIso f)).hom x✝ = ↑f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
⊢ homeoOfIso (isoOfHomeo f) = f
[PROOFSTEP]
ext
[GOAL]
case H
X Y : Profinite
f✝ : X ⟶ Y
f : ↑X.toCompHaus.toTop ≃ₜ ↑Y.toCompHaus.toTop
x✝ : ↑X.toCompHaus.toTop
⊢ ↑(homeoOfIso (isoOfHomeo f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f
[PROOFSTEP]
dsimp [Function.Surjective]
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget Profinite).obj Y), ∃ a, ↑f a = b
[PROOFSTEP]
contrapose!
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget Profinite).obj X), ↑f a ≠ b) → ¬Epi f
[PROOFSTEP]
rintro ⟨y, hy⟩ hf
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
⊢ False
[PROOFSTEP]
skip
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
⊢ False
[PROOFSTEP]
let C := Set.range f
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
⊢ False
[PROOFSTEP]
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
⊢ False
[PROOFSTEP]
let U := Cᶜ
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ False
[PROOFSTEP]
have hyU : y ∈ U := by
  refine' Set.mem_compl _
  rintro ⟨y', hy'⟩
  exact hy y' hy'
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ y ∈ U
[PROOFSTEP]
refine' Set.mem_compl _
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ ¬y ∈ C
[PROOFSTEP]
rintro ⟨y', hy'⟩
[GOAL]
case intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
y' : (forget Profinite).obj X
hy' : ↑f y' = y
⊢ False
[PROOFSTEP]
exact hy y' hy'
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
⊢ False
[PROOFSTEP]
have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
[GOAL]
case mp.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
⊢ False
[PROOFSTEP]
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
[PROOFSTEP]
classical
let Z := of (ULift.{u} <| Fin 2)
let g : Y ⟶ Z := ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ Z := ⟨fun _ => ⟨1⟩, continuous_const⟩
have H : h = g := by
  rw [← cancel_epi f]
  ext x
  apply ULift.ext
  dsimp [LocallyConstant.ofClopen]
  rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk, Function.comp_apply, if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
apply_fun fun e => (e y).down at H
dsimp [LocallyConstant.ofClopen] at H
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
exact top_ne_bot H
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
[PROOFSTEP]
let Z := of (ULift.{u} <| Fin 2)
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
⊢ False
[PROOFSTEP]
let g : Y ⟶ Z := ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
⊢ False
[PROOFSTEP]
let h : Y ⟶ Z := ⟨fun _ => ⟨1⟩, continuous_const⟩
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
⊢ False
[PROOFSTEP]
have H : h = g := by
  rw [← cancel_epi f]
  ext x
  apply ULift.ext
  dsimp [LocallyConstant.ofClopen]
  rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk, Function.comp_apply, if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
⊢ h = g
[PROOFSTEP]
rw [← cancel_epi f]
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
⊢ f ≫ h = f ≫ g
[PROOFSTEP]
ext x
[GOAL]
case w
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
x : (forget Profinite).obj X
⊢ ↑(f ≫ h) x = ↑(f ≫ g) x
[PROOFSTEP]
apply ULift.ext
[GOAL]
case w.h
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
x : (forget Profinite).obj X
⊢ (↑(f ≫ h) x).down = (↑(f ≫ g) x).down
[PROOFSTEP]
dsimp [LocallyConstant.ofClopen]
[GOAL]
case w.h
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
x : (forget Profinite).obj X
⊢ (↑(f ≫ ContinuousMap.mk fun x => { down := 1 }) x).down =
    (↑(f ≫ ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) x).down
[PROOFSTEP]
rw [comp_apply, ContinuousMap.coe_mk, comp_apply, ContinuousMap.coe_mk, Function.comp_apply, if_neg]
[GOAL]
case w.h.hnc
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
x : (forget Profinite).obj X
⊢ ¬↑f x ∈ V
[PROOFSTEP]
refine' mt (fun α => hVU α) _
[GOAL]
case w.h.hnc
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
x : (forget Profinite).obj X
⊢ ¬↑f x ∈ U
[PROOFSTEP]
simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
H : h = g
⊢ False
[PROOFSTEP]
apply_fun fun e => (e y).down at H
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
H : (↑h y).down = (↑g y).down
⊢ False
[PROOFSTEP]
dsimp [LocallyConstant.ofClopen] at H
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
H :
  (↑(ContinuousMap.mk fun x => { down := 1 }) y).down =
    (↑(ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) y).down
⊢ False
[PROOFSTEP]
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
[GOAL]
case mp.intro.intro.intro.intro
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), ↑f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ↑f
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ((forget Profinite).obj Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift (Fin 2))
g : Y ⟶ Z := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ Z := ContinuousMap.mk fun x => { down := 1 }
H : { down := 1 }.down = { down := 0 }.down
⊢ False
[PROOFSTEP]
exact top_ne_bot H
[GOAL]
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f
[PROOFSTEP]
rw [← CategoryTheory.epi_iff_surjective]
[GOAL]
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi ↑f → Epi f
[PROOFSTEP]
apply (forget Profinite).epi_of_epi_map
[GOAL]
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Mono f → Function.Injective ↑f
[PROOFSTEP]
intro h
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
h : Mono f
⊢ Function.Injective ↑f
[PROOFSTEP]
haveI : Limits.PreservesLimits profiniteToCompHaus := inferInstance
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
h : Mono f
this : Limits.PreservesLimits profiniteToCompHaus
⊢ Function.Injective ↑f
[PROOFSTEP]
haveI : Mono (profiniteToCompHaus.map f) := inferInstance
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
h : Mono f
this✝ : Limits.PreservesLimits profiniteToCompHaus
this : Mono (profiniteToCompHaus.map f)
⊢ Function.Injective ↑f
[PROOFSTEP]
rw [← CompHaus.mono_iff_injective]
[GOAL]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
h : Mono f
this✝ : Limits.PreservesLimits profiniteToCompHaus
this : Mono (profiniteToCompHaus.map f)
⊢ Mono f
[PROOFSTEP]
assumption
[GOAL]
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Function.Injective ↑f → Mono f
[PROOFSTEP]
rw [← CategoryTheory.mono_iff_injective]
[GOAL]
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Mono ↑f → Mono f
[PROOFSTEP]
apply (forget Profinite).mono_of_mono_map