From c58c018d161481b4cbde118a05bfbb6b8b0bc06b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 10 Aug 2026 18:26:15 +0530 Subject: [PATCH] feat(CategoryTheory/Galois): fix namespace --- Mathlib/CategoryTheory/Galois/Basic.lean | 26 ++++++++++++------- .../CategoryTheory/Galois/Decomposition.lean | 5 ++-- Mathlib/CategoryTheory/Galois/Examples.lean | 2 +- .../CategoryTheory/Galois/GaloisObjects.lean | 8 +++--- 4 files changed, 24 insertions(+), 17 deletions(-) diff --git a/Mathlib/CategoryTheory/Galois/Basic.lean b/Mathlib/CategoryTheory/Galois/Basic.lean index 36a41aab863f40..4915e04fc27a15 100644 --- a/Mathlib/CategoryTheory/Galois/Basic.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Galois/Decomposition.lean b/Mathlib/CategoryTheory/Galois/Decomposition.lean index 371f0121d8f359..b03cf9bef72a10 100644 --- a/Mathlib/CategoryTheory/Galois/Decomposition.lean +++ b/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. -/ diff --git a/Mathlib/CategoryTheory/Galois/Examples.lean b/Mathlib/CategoryTheory/Galois/Examples.lean index 7894942aacce32..1e75249e3d3f9e 100644 --- a/Mathlib/CategoryTheory/Galois/Examples.lean +++ b/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) diff --git a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean index ce474a0bd36806..ece804238b8013 100644 --- a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean +++ b/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]