English
If H is an open subset of Aut F with 1 in H, there exists a finite set I of connected objects such that any Aut F element that acts identically on all F.obj X for X in I lies in H.
Русский
Если H — открытое подмножество Aut F и 1 ∈ H, существует конечное множество подключенных объектов I, так что любой элемент Aut F, действующий как единичный на всех F.obj X при X∈I, принадлежит H.
LaTeX
$$$\exists I: Set C\,\big(\#I<\infty\big)\;\wedge\; (\forall X\in I, IsConnected X) \land\ (\forall \sigma: Aut F, (\forall X: I, \sigma.hom.app X = 1) \Rightarrow \sigma \in H)$$$
Lean4
/-- If `H` is an open subset of `Aut F` such that `1 ∈ H`, there exists a finite
set `I` of connected objects of `C` such that every `σ : Aut F` that induces the identity
on `F.obj X` for all `X ∈ I` is contained in `H`. In other words: The kernel
of the evaluation map `Aut F →* ∏ X : I ↦ Aut (F.obj X)` is contained in `H`.
-/
theorem exists_set_ker_evaluation_subset_of_isOpen {H : Set (Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) :
∃ (I : Set C) (_ : Fintype I),
(∀ X ∈ I, IsConnected X) ∧ (∀ σ : Aut F, (∀ X : I, σ.hom.app X = 𝟙 (F.obj X)) → σ ∈ H) :=
by
obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h
obtain ⟨I, u, ho, ha⟩ := isOpen_pi_iff.mp hUopen 1 h1
choose fι ff fc h4 h5 h6 using (fun X : I => has_decomp_connected_components X.val)
refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
· rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩
obtain ⟨i, rfl⟩ := hA2
exact h5 Y i
· refine fun σ h ↦ ha (fun X XinI ↦ ?_)
suffices h : autEmbedding F σ X = 1 by
rw [h]
exact (ho X XinI).right
have h : σ.hom.app X = 𝟙 (F.obj X) :=
by
have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
ext x
obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ :=
Limits.FintypeCat.jointly_surjective (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _
(Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
rw [FintypeCat.id_apply, ← ha, FunctorToFintypeCat.naturality]
simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
exact Iso.ext h
