[Merged by Bors] - chore(CategoryTheory/Galois): fix namespace for getFiberFunctor

Mathlib/CategoryTheory/Galois/Basic.lean

@@ -411,39 +411,45 @@ end PreGaloisCategory
 /-- A `PreGaloisCategory` is a `GaloisCategory` if it admits a fiber functor. -/
 class GaloisCategory (C : Type u₁) [Category.{u₂, u₁} C] : Prop
     extends PreGaloisCategory C where
-  hasFiberFunctor : ∃ F : C ⥤ FintypeCat.{u₂}, Nonempty (PreGaloisCategory.FiberFunctor F)
+  hasFiberFunctor (C) : ∃ F : C ⥤ FintypeCat.{u₂}, PreGaloisCategory.FiberFunctor F
+
+/-- Arbitrarily choose a fiber functor for a Galois category using choice. -/
+noncomputable def GaloisCategory.getFiberFunctor
+    (C : Type u₁) [Category.{u₂, u₁} C] [GaloisCategory C] : C ⥤ FintypeCat.{u₂} :=
+  Classical.choose <| hasFiberFunctor C
+
+open GaloisCategory
+
+@[deprecated (since := "2026-08-10")]
+alias PreGaloisCategory.GaloisCategory.getFiberFunctor := getFiberFunctor
 
 namespace PreGaloisCategory
 
 variable (C : Type u₁) [Category.{u₂, u₁} C] [GaloisCategory C]
 
-/-- Arbitrarily choose a fiber functor for a Galois category using choice. -/
-noncomputable def GaloisCategory.getFiberFunctor : C ⥤ FintypeCat.{u₂} :=
-  Classical.choose <| @GaloisCategory.hasFiberFunctor C _ _
-
 /-- The arbitrarily chosen fiber functor `GaloisCategory.getFiberFunctor` is a fiber functor. -/
-noncomputable instance : FiberFunctor (GaloisCategory.getFiberFunctor C) :=
-  Classical.choice <| Classical.choose_spec (@GaloisCategory.hasFiberFunctor C _ _)
+noncomputable instance : FiberFunctor (getFiberFunctor C) :=
+  Classical.choose_spec (hasFiberFunctor C)
 
 variable {C}
 
 /-- In a `GaloisCategory` the set of morphisms out of a connected object is finite. -/
 instance (A X : C) [IsConnected A] : Finite (A ⟶ X) := by
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
   apply Finite.of_injective (fun f ↦ F.map f a)
   exact evaluation_injective_of_isConnected F A X a
 
 /-- In a `GaloisCategory` the set of automorphism of a connected object is finite. -/
 instance (A : C) [IsConnected A] : Finite (Aut A) := by
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
   apply Finite.of_injective (fun f ↦ F.map f.hom a)
   exact evaluation_aut_injective_of_isConnected F A a
 
 /-- Coproduct inclusions are monic in Galois categories. -/
 instance : MonoCoprod C := by
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   exact MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono F
 
 end PreGaloisCategory

Mathlib/CategoryTheory/Galois/Decomposition.lean

@@ -39,13 +39,12 @@ universe u₁ u₂ w
 
 namespace CategoryTheory
 
-open Limits CategoryTheory.Functor
+open Limits CategoryTheory.Functor GaloisCategory
 
 variable {C : Type u₁} [Category.{u₂} C]
 
 namespace PreGaloisCategory
 
-
 section Decomposition
 
 /-! ### Decomposition in connected components
@@ -119,7 +118,7 @@ private lemma has_decomp_connected_components_aux (F : C ⥤ FintypeCat.{w}) [Fi
 theorem has_decomp_connected_components (X : C) :
     ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (_ : IsColimit (Cofan.mk X g)),
       (∀ i, IsConnected (f i)) ∧ Finite ι := by
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   exact has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl
 
 /-- In a Galois category, every object is the sum of connected objects. -/

Mathlib/CategoryTheory/Galois/Examples.lean

@@ -103,7 +103,7 @@ noncomputable instance : FiberFunctor (forget₂ (Action FintypeCat G) FintypeCa
 
 /-- The category of finite `G`-sets is a `GaloisCategory`. -/
 instance : GaloisCategory (Action FintypeCat G) where
-  hasFiberFunctor := ⟨Action.forget FintypeCat G, ⟨inferInstance⟩⟩
+  hasFiberFunctor := ⟨Action.forget FintypeCat G, inferInstance⟩
 
 /-- The `G`-action on a connected finite `G`-set is transitive. -/
 theorem Action.pretransitive_of_isConnected (X : Action FintypeCat G)

Mathlib/CategoryTheory/Galois/GaloisObjects.lean

@@ -33,6 +33,8 @@ universe u₁ u₂ v₁ v₂ v w
 
 namespace CategoryTheory
 
+open GaloisCategory
+
 namespace PreGaloisCategory
 
 open Limits CategoryTheory.Functor
@@ -139,7 +141,7 @@ section AutMap
 of `A`, there exists a unique automorphism of `B` making the canonical diagram commute. -/
 lemma 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
+  let F := 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)
@@ -187,7 +189,7 @@ lemma autMap_comp {X Y Z : C} [IsConnected X] [IsGalois Y] [IsGalois Z] (f : X 
 lemma autMap_surjective_of_isGalois {A B : C} [IsGalois A] [IsGalois B] (f : A ⟶ B) :
     Function.Surjective (autMap f) := by
   intro σ
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
   obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f a))
   obtain ⟨τ, (hτ : F.map τ.hom a = a')⟩ := MulAction.exists_smul_eq (Aut A) a a'
@@ -199,7 +201,7 @@ set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma autMap_apply_mul {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ τ : Aut A) :
     autMap f (σ * τ) = autMap f σ * autMap f τ := by
-  let F := GaloisCategory.getFiberFunctor C
+  let F := getFiberFunctor C
   obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A
   apply evaluation_aut_injective_of_isConnected F (B : C) (F.map f a)
   simp [Aut.Aut_mul_def]