case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ((forget Profinite).map f)

case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ((forget Profinite).map f) → Epi f
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ((forget Profinite).map f)
constructor
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget Profinite).obj Y), ∃ a, (forget Profinite).map f a = b
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ((forget Profinite).map f)
dsimp [Function.Surjective]
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ b) → ¬Epi f
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi f → ∀ (b : (forget Profinite).obj Y), ∃ a, (forget Profinite).map f a = b
contrapose!
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), (forget Profinite).map f a ≠ y
hf : Epi f
⊢ False
case mp
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ (∃ b, ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ b) → ¬Epi f
rintro ⟨y, hy⟩ hf
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), (forget Profinite).map f a ≠ y
hf : Epi f
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
⊢ False
skip
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
⊢ False
let C := Set.range f
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
⊢ False
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
⊢ False
let U := Cᶜ
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ False
have hyU : y ∈ U := by
  refine' Set.mem_compl _
  rintro ⟨y', hy'⟩
  exact hy y' hy'
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
⊢ False
have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
⊢ False
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
no goals
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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]
    simp only [FunctorToTypes.map_comp_apply, forget_ContinuousMap_mk, Function.comp_apply]
    rw [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 [if_pos hyV] at H
  exact top_ne_bot H
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ ¬y ∈ C
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ y ∈ U
refine' Set.mem_compl _
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
y' : (forget Profinite).obj X
hy' : (forget Profinite).map f y' = y
⊢ False
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
⊢ ¬y ∈ C
rintro ⟨y', hy'⟩
no goals
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map f)
hC : IsClosed C
U : Set ((forget Profinite).obj Y) := Cᶜ
y' : (forget Profinite).obj X
hy' : (forget Profinite).map f y' = y
⊢ False
exact hy y' hy'
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
let Z := of (ULift.{u} <| Fin 2)
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
let g : Y ⟶ Z := ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
let h : Y ⟶ Z := ⟨fun _ => ⟨1⟩, continuous_const⟩
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
have H : h = g := by
  rw [← cancel_epi f]
  ext x
  apply ULift.ext
  dsimp [LocallyConstant.ofClopen]
  simp only [FunctorToTypes.map_comp_apply, forget_ContinuousMap_mk, Function.comp_apply]
  rw [if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : ((forget Profinite).map h y).down = ((forget Profinite).map g y).down
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
apply_fun fun e => (e y).down  at H
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : 1 = if y ∈ V then 0 else 1
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : ((forget Profinite).map h y).down = ((forget Profinite).map g y).down
⊢ False
dsimp [LocallyConstant.ofClopen] at H
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : 1 = 0
⊢ False
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : 1 = if y ∈ V then 0 else 1
⊢ False
rw [if_pos hyV] at H
no goals
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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 : 1 = 0
⊢ False
exact top_ne_bot H
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
rw [← cancel_epi f]
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ (forget Profinite).map (f ≫ h) x = (forget Profinite).map (f ≫ g) x
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
y : (forget Profinite).obj Y
hy : ∀ (a : (forget Profinite).obj X), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
ext x
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ((forget Profinite).map (f ≫ h) x).down = ((forget Profinite).map (f ≫ g) x).down
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ (forget Profinite).map (f ≫ h) x = (forget Profinite).map (f ≫ g) x
apply ULift.ext
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ((forget Profinite).map (f ≫ ContinuousMap.mk fun x => { down := 1 }) x).down =
    ((forget Profinite).map (f ≫ ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) x).down
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ((forget Profinite).map (f ≫ h) x).down = ((forget Profinite).map (f ≫ g) x).down
dsimp [LocallyConstant.ofClopen]
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ 1 = if (forget Profinite).map f x ∈ V then 0 else 1
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ((forget Profinite).map (f ≫ ContinuousMap.mk fun x => { down := 1 }) x).down =
    ((forget Profinite).map (f ≫ ContinuousMap.mk (ULift.up ∘ fun x => if x ∈ V then 0 else 1)) x).down
simp only [FunctorToTypes.map_comp_apply, forget_ContinuousMap_mk, Function.comp_apply]
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ¬(forget Profinite).map f x ∈ V
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ 1 = if (forget Profinite).map f x ∈ V then 0 else 1
rw [if_neg]
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ¬(forget Profinite).map f x ∈ U
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ¬(forget Profinite).map f x ∈ V
refine' mt (fun α => hVU α) _
no goals
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), (forget Profinite).map f a ≠ y
hf : Epi f
C : Set ((forget Profinite).obj Y) := Set.range ((forget Profinite).map 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
⊢ ¬(forget Profinite).map f x ∈ U
simp only [Set.mem_range_self, not_true, not_false_iff, Set.mem_compl_iff]
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi ((forget Profinite).map f) → Epi f
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Function.Surjective ((forget Profinite).map f) → Epi f
rw [← CategoryTheory.epi_iff_surjective]
no goals
case mpr
X✝ Y✝ : Profinite
f✝ : X✝ ⟶ Y✝
X Y : Profinite
f : X ⟶ Y
⊢ Epi ((forget Profinite).map f) → Epi f
apply (forget Profinite).epi_of_epi_map