English
In the fully Galois context, a mono lift exists with Z, f, u as in the mono lifting lemma, ensuring the compatibility condition with i.
Русский
В полно-Галуа контексте существует моно-подъём с Z, f, u, удовлетворяющий условию совместимости с i.
LaTeX
$$$\\exists Z:\\, C, \\exists f:\\, Z \\to X, \\exists u:\\, Y \\cong (\\mathrm{functorToAction} F).obj Z, \\text{Mono } f \\land i = u.hom \\circ (\\mathrm{functorToAction} F).map f$$$
Lean4
/-- Let `X` be an object of a Galois category with fiber functor `F` and `Y` a sub-`Aut F`-set
of `F.obj X`, on which `Aut F` acts transitively (i.e. which is connected in the Galois category
of finite `Aut F`-sets). Then there exists a connected sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.
For a version without the connectedness assumption, see `exists_lift_of_mono`.
-/
theorem exists_lift_of_mono_of_isConnected (X : C) (Y : Action FintypeCat.{u} (Aut F))
(i : Y ⟶ (functorToAction F).obj X) [Mono i] [IsConnected Y] :
∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f :=
by
obtain ⟨y⟩ := nonempty_fiber_of_isConnected (forget₂ _ FintypeCat) Y
obtain ⟨Z, f, z, hz, hc, hm⟩ := fiber_in_connected_component F X (i.hom y)
have : IsConnected ((functorToAction F).obj Z) := PreservesIsConnected.preserves
obtain ⟨u, hu⟩ :=
connected_component_unique (forget₂ (Action FintypeCat (Aut F)) FintypeCat) (B := (functorToAction F).obj Z) y z i
((functorToAction F).map f) hz.symm
refine ⟨Z, f, u, hc, hm, ?_⟩
apply
evaluation_injective_of_isConnected (forget₂ (Action FintypeCat (Aut F)) FintypeCat) Y ((functorToAction F).obj X) y
suffices h : i.hom y = F.map f z by simpa [hu]
exact hz.symm
