English
As above, the evaluation bijectivity holds for the same data; i.e., Aut A → F.obj A is bijective when A is Galois.
Русский
Как и выше, биекция оценки сохраняется при тех же условиях; Aut A → F.obj A биекция, когда A галуа.
LaTeX
$$$\\text{Bijective}(\\mathrm{Aut}\\,A \\to F.obj A)$$$
Lean4
/-- For a morphism from a connected object `A` to a Galois object `B` and an automorphism
of `A`, there exists a unique automorphism of `B` making the canonical diagram commute. -/
theorem exists_autMap {A B : C} (f : A ⟶ B) [IsConnected A] [IsGalois B] (σ : Aut A) :
∃! (τ : Aut B), f ≫ τ.hom = σ.hom ≫ f :=
by
let F := GaloisCategory.getFiberFunctor C
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
refine ⟨?_, ?_, ?_⟩
· exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)
· apply evaluation_injective_of_isConnected F A B a
simp
· intro τ hτ
apply evaluation_aut_injective_of_isConnected F B (F.map f a)
simpa using congr_fun (F.congr_map hτ) a
