J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let U := f ⁻¹' {0}
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
case intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
obtain ⟨j, V, hV, h⟩ := exists_clopen_of_cofiltered C hC hU
case intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.ofClopen hV)
case intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
use j, LocallyConstant.ofClopen hV
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.ofClopen hV)) ⁻¹' {0}
case intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.ofClopen hV)
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.ofClopen hV) ∘ (forget Profinite).map (C.π.1 j) ⁻¹' {0}
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.ofClopen hV)) ⁻¹' {0}
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j).continuous]
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = (forget Profinite).map (C.π.1 j) ⁻¹' (↑(LocallyConstant.ofClopen hV) ⁻¹' {0})
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.ofClopen hV) ∘ (forget Profinite).map (C.π.1 j) ⁻¹' {0}
conv_rhs => rw [Set.preimage_comp]
no goals
case intro.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = (forget Profinite).map (C.π.app j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = (forget Profinite).map (C.π.1 j) ⁻¹' (↑(LocallyConstant.ofClopen hV) ⁻¹' {0})
rw [LocallyConstant.ofClopen_fiber_zero hV, ← h]