Definition and basic properties of Galois categories #
We define the notion of a Galois category and a fiber functor as in SGA1, following the definitions in Lenstras notes (see below for a reference).
Main definitions #
PreGaloisCategory: defining properties of Galois categories not involving a fiber functorFiberFunctor: a fiber functor from aPreGaloisCategorytoFintypeCatGaloisCategory: aPreGaloisCategorythat admits aFiberFunctorIsConnected: an object of a category is connected if it is not initial and does not have non-trivial subobjects
Implementation details #
We mostly follow Def 3.1 in Lenstras notes. In axiom (G3) we omit the factorisation of morphisms in epimorphisms and monomorphisms as this is not needed for the proof of the fundamental theorem on Galois categories (and then follows from it).
References #
- [Len]: H. W. Lenstra. Galois theory for schemes.
A category C is a PreGalois category if it satisfies all properties
of a Galois category in the sense of SGA1 that do not involve a fiber functor.
A Galois category should furthermore admit a fiber functor.
The only difference between [PreGaloisCategory C] (F : C ⥤ FintypeCat) [FiberFunctor F] and
[GaloisCategory C] is that the former fixes one fiber functor F.
Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3)
- hasTerminal : CategoryTheory.Limits.HasTerminal C
Chas a terminal object (G1). - hasPullbacks : CategoryTheory.Limits.HasPullbacks C
Chas pullbacks (G1). - hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
Chas finite coproducts (G2). - hasQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
Chas quotients by finite groups (G2). - monoInducesIsoOnDirectSummand {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i] : ∃ (Z : C) (u : Z ⟶ Y), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
Every monomorphism in
Cinduces an isomorphism on a direct summand (G3).
Instances
class
CategoryTheory.PreGaloisCategory.FiberFunctor
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.PreGaloisCategory C]
(F : CategoryTheory.Functor C FintypeCat)
:
Definition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)
- preservesTerminalObjects : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
Fpreserves terminal objects (G4). - preservesPullbacks : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F
Fpreserves pullbacks (G4). - preservesFiniteCoproducts : CategoryTheory.Limits.PreservesFiniteCoproducts F
Fpreserves finite coproducts (G5). - preservesEpis : F.PreservesEpimorphisms
Fpreserves epimorphisms (G5). - preservesQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F
Fpreserves quotients by finite groups (G5). - reflectsIsos : F.ReflectsIsomorphisms
Freflects isomorphisms (G6).
Instances
class
CategoryTheory.PreGaloisCategory.IsConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(X : C)
:
An object of a category C is connected if it is not initial
and has no non-trivial subobjects. Lenstra, 3.12.
- notInitial : CategoryTheory.Limits.IsInitial X → False
Xis not an initial object. - noTrivialComponent (Y : C) (i : Y ⟶ X) [CategoryTheory.Mono i] : (CategoryTheory.Limits.IsInitial Y → False) → CategoryTheory.IsIso i
Xhas no non-trivial subobjects.
Instances
class
CategoryTheory.PreGaloisCategory.PreservesIsConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{D : Type v₁}
[CategoryTheory.Category.{v₂, v₁} D]
(F : CategoryTheory.Functor C D)
:
A functor is said to preserve connectedness if whenever X : C is connected,
also F.obj X is connected.
- preserves {X : C} [CategoryTheory.PreGaloisCategory.IsConnected X] : CategoryTheory.PreGaloisCategory.IsConnected (F.obj X)
F.obj Xis connected ifXis connected.
Instances
instance
CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.PreGaloisCategory C]
{G : Type u_1}
[Group G]
[Finite G]
:
instance
CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{F : CategoryTheory.Functor C FintypeCat}
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{G : Type u_1}
[Group G]
[Finite G]
:
Fiber functors preserve quotients by finite groups in arbitrary universes.
instance
CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{F : CategoryTheory.Functor C FintypeCat}
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
:
F.ReflectsMonomorphisms
Fiber functors reflect monomorphisms.
instance
CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCat
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{F : CategoryTheory.Functor C FintypeCat}
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
:
F.Faithful
Fiber functors are faithful.
theorem
CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
{F : CategoryTheory.Functor C FintypeCat}
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(E : CategoryTheory.Functor FintypeCat FintypeCat)
[E.IsEquivalence]
:
If F is a fiber functor and E is an equivalence between categories of finite types,
then F ⋙ E is again a fiber functor.
instance
CategoryTheory.PreGaloisCategory.instMulActionAutFunctorFintypeCatαFintypeObj
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
(X : C)
:
MulAction (CategoryTheory.Aut F) ↑(F.obj X)
The canonical action of Aut F on the fiber of each object.
theorem
CategoryTheory.PreGaloisCategory.mulAction_def
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
{X : C}
(σ : CategoryTheory.Aut F)
(x : ↑(F.obj X))
:
theorem
CategoryTheory.PreGaloisCategory.mulAction_naturality
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
{X Y : C}
(σ : CategoryTheory.Aut F)
(f : X ⟶ Y)
(x : ↑(F.obj X))
:
theorem
CategoryTheory.PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_initial
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(X : C)
(hc : ¬CategoryTheory.PreGaloisCategory.IsConnected X)
(hi : CategoryTheory.Limits.IsInitial X → False)
:
∃ (Y : C) (v : Y ⟶ X), (CategoryTheory.Limits.IsInitial Y → False) ∧ CategoryTheory.Mono v ∧ ¬CategoryTheory.IsIso v
An object that is neither initial or connected has a non-trivial subobject.
theorem
CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
{X Y : C}
(i : X ≅ Y)
:
The cardinality of the fiber is preserved under isomorphisms.
theorem
CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X : C)
:
Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↑(F.obj X)
An object is initial if and only if its fiber is empty.
theorem
CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X : C)
:
CategoryTheory.Limits.IsInitial X → False ↔ Nonempty ↑(F.obj X)
An object is not initial if and only if its fiber is nonempty.
theorem
CategoryTheory.PreGaloisCategory.not_initial_of_inhabited
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X : C}
(x : ↑(F.obj X))
(h : CategoryTheory.Limits.IsInitial X)
:
An object whose fiber is inhabited is not initial.
instance
CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X : C)
[CategoryTheory.PreGaloisCategory.IsConnected X]
:
Nonempty ↑(F.obj X)
The fiber of a connected object is nonempty.
noncomputable def
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(f g : X ⟶ Y)
:
↑(F.obj (CategoryTheory.Limits.equalizer f g)) ≃ { x : ↑(F.obj X) // F.map f x = F.map g x }
The fiber of the equalizer of f g : X ⟶ Y is equivalent to the set of agreement of f
and g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
{f g : X ⟶ Y}
(x : ↑(F.obj X))
(h : F.map f x = F.map g x)
:
F.map (CategoryTheory.Limits.equalizer.ι f g)
((CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x
noncomputable def
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X A B : C}
(f : A ⟶ X)
(g : B ⟶ X)
:
↑(F.obj (CategoryTheory.Limits.pullback f g)) ≃ { p : ↑(F.obj A) × ↑(F.obj B) // F.map f p.1 = F.map g p.2 }
The fiber of the pullback is the fiber product of the fibers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X A B : C}
{f : A ⟶ X}
{g : B ⟶ X}
(a : ↑(F.obj A))
(b : ↑(F.obj B))
(h : F.map f a = F.map g b)
:
F.map (CategoryTheory.Limits.pullback.fst f g)
((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a
@[simp]
theorem
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X A B : C}
{f : A ⟶ X}
{g : B ⟶ X}
(a : ↑(F.obj A))
(b : ↑(F.obj B))
(h : F.map f a = F.map g b)
:
F.map (CategoryTheory.Limits.pullback.snd f g)
((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b
noncomputable def
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X Y : C)
:
The fiber of the binary product is the binary product of the fibers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(x : ↑(F.obj X))
(y : ↑(F.obj Y))
:
F.map CategoryTheory.Limits.prod.fst ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = x
@[simp]
theorem
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(x : ↑(F.obj X))
(y : ↑(F.obj Y))
:
F.map CategoryTheory.Limits.prod.snd ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = y
theorem
CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(A X : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
(a : ↑(F.obj A))
:
Function.Injective fun (f : A ⟶ X) => F.map f a
The evaluation map is injective for connected objects.
theorem
CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(A : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
(a : ↑(F.obj A))
:
Function.Injective fun (f : CategoryTheory.Aut A) => F.map f.hom a
The evaluation map on automorphisms is injective for connected objects.
theorem
CategoryTheory.PreGaloisCategory.epi_of_nonempty_of_isConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X A : C}
[CategoryTheory.PreGaloisCategory.IsConnected A]
[h : Nonempty ↑(F.obj X)]
(f : X ⟶ A)
:
A morphism from an object X with non-empty fiber to a connected object A is an
epimorphism.
theorem
CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
Function.Surjective (F.map f)
An epimorphism induces a surjective map on fibers.
theorem
CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X A : C}
[Nonempty ↑(F.obj X)]
[CategoryTheory.PreGaloisCategory.IsConnected A]
(f : X ⟶ A)
:
Function.Surjective (F.map f)
instance
CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{ι : Type u_1}
[Finite ι]
(X : ι → C)
[∀ (i : ι), Nonempty ↑(F.obj (X i))]
:
If X : ι → C is a finite family of objects with non-empty fiber, then
also ∏ᶜ X has non-empty fiber.
theorem
CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
(h : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y))
:
A mono between objects with equally sized fibers is an iso.
theorem
CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
{X Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
(h : ¬CategoryTheory.IsIso f)
:
Along a mono that is not an iso, the cardinality of the fiber strictly increases.
theorem
CategoryTheory.PreGaloisCategory.non_zero_card_fiber_of_not_initial
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X : C)
(h : CategoryTheory.Limits.IsInitial X → False)
:
The cardinality of the fiber of a not-initial object is non-zero.
theorem
CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(X Y : C)
:
The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers.
theorem
CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(A X : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
:
The cardinality of morphisms A ⟶ X is smaller than the cardinality of
the fiber of the target if the source is connected.
theorem
CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
(F : CategoryTheory.Functor C FintypeCat)
[CategoryTheory.PreGaloisCategory C]
[CategoryTheory.PreGaloisCategory.FiberFunctor F]
(A : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
:
Nat.card (CategoryTheory.Aut A) ≤ Nat.card ↑(F.obj A)
If A is connected, the cardinality of Aut A is smaller than the cardinality of the
fiber of A.
class
CategoryTheory.GaloisCategory
(C : Type u₁)
[CategoryTheory.Category.{u₂, u₁} C]
extends CategoryTheory.PreGaloisCategory C :
A PreGaloisCategory is a GaloisCategory if it admits a fiber functor.
- hasQuotientsByFiniteGroups (G : Type u₂) [Group G] [Finite G] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
- monoInducesIsoOnDirectSummand {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i] : ∃ (Z : C) (u : Z ⟶ Y), Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
- hasFiberFunctor : ∃ (F : CategoryTheory.Functor C FintypeCat), Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)
Instances
noncomputable def
CategoryTheory.PreGaloisCategory.GaloisCategory.getFiberFunctor
(C : Type u₁)
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.GaloisCategory C]
:
Arbitrarily choose a fiber functor for a Galois category using choice.
Instances For
instance
CategoryTheory.PreGaloisCategory.instFiberFunctorGetFiberFunctor
(C : Type u₁)
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.GaloisCategory C]
:
The arbitrarily chosen fiber functor GaloisCategory.getFiberFunctor is a fiber functor.
instance
CategoryTheory.PreGaloisCategory.instFiniteHomOfIsConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.GaloisCategory C]
(A X : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
:
In a GaloisCategory the set of morphisms out of a connected object is finite.
instance
CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.GaloisCategory C]
(A : C)
[CategoryTheory.PreGaloisCategory.IsConnected A]
:
In a GaloisCategory the set of automorphism of a connected object is finite.
instance
CategoryTheory.PreGaloisCategory.instMonoCoprod
{C : Type u₁}
[CategoryTheory.Category.{u₂, u₁} C]
[CategoryTheory.GaloisCategory C]
:
Coproduct inclusions are monic in Galois categories.