CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups
theorem CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C]
(G : Type u₂) [inst_1 : Group G] [inst_2 : Finite G],
CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
The theorem `CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups` states that for any category `C` of type `u₁` which is also a PreGalois category, for any type `G` of a group that is finite, `C` has colimits of the shape `CategoryTheory.SingleObj G`. Here `CategoryTheory.SingleObj G` denotes the category with one object and morphisms from this object to itself given by elements of the group `G`. The colimits of a given shape in a category provide a way of gluing objects together along mappings. In this case, the theorem states that we can construct "quotients" of objects in `C` by the action of a finite group.
More concisely: In any PreGalois category `C` of type `u₁`, there exists a colimit for every finite group `G` with one object, yielding quotients of objects in `C` by the action of `G`.
|
CategoryTheory.PreGaloisCategory.hasFiniteCoproducts
theorem CategoryTheory.PreGaloisCategory.hasFiniteCoproducts :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C],
CategoryTheory.Limits.HasFiniteCoproducts C
This theorem states that for any type `C`, given that `C` is a category (as per the `CategoryTheory.Category` class) and a pre-Galois category (as per the `CategoryTheory.PreGaloisCategory` class), `C` has finite coproducts. In the context of category theory, having finite coproducts means that for any finite collection of objects in category `C`, their coproduct (a kind of "sum" of objects in a category) exists.
More concisely: If `C` is a pre-Galois category in Lean 4, then `C` has finite coproducts.
|
CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty
theorem CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.PreGaloisCategory C]
(F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↑(F.obj X)
The theorem `CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty` states that for any category `C` equipped with a structure of a PreGalois category and any functor `F` from `C` to the category of finite types `FintypeCat`, an object `X` in `C` is initial if and only if the fiber of `X` under the functor `F` is empty. The fiber of an object under a functor is the inverse image of the object under the functor, and here we use the type `IsEmpty` to represent the empty type, so `IsEmpty ↑(F.obj X)` means the fiber of `X` under `F` is empty. Here, initial objects are characterized specifically via the property of having a colimiting cocone induced on the empty diagram.
More concisely: In a PreGalois category equipped with a functor to the category of finite types, an object is initial if and only if its fiber under the functor is empty.
|
CategoryTheory.PreGaloisCategory.hasTerminal
theorem CategoryTheory.PreGaloisCategory.hasTerminal :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C],
CategoryTheory.Limits.HasTerminal C
This theorem states that for any type `C`, if `C` forms a category under some instance and is a PreGalois category, then it possesses a terminal object. In the context of category theory, a terminal object is an object in a category such that there exists a unique morphism from any other object in the category to it.
More concisely: If `C` is a PreGalois category with an instance of the category structure, then `C` has a terminal object with the unique property that for every object `X` in `C`, there exists a unique morphism from `X` to the terminal object.
|
CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand
theorem CategoryTheory.PreGaloisCategory.monoInducesIsoOnDirectSummand :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C] {X Y : C}
(i : X ⟶ Y) [inst_1 : CategoryTheory.Mono i],
∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
This theorem states that in any Pre-Galois category `C`, for any objects `X` and `Y` and any monomorphism `i` from `X` to `Y`, there exists an object `Z` and a morphism `u` such that the binary cofan formed by `i` and `u` is a colimit. In simpler terms, every monomorphism in a Pre-Galois category induces an isomorphism on some direct summand.
More concisely: In a Pre-Galois category, every monomorphism induces an isomorphism on some direct summand.
|
CategoryTheory.PreGaloisCategory.hasPullbacks
theorem CategoryTheory.PreGaloisCategory.hasPullbacks :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [self : CategoryTheory.PreGaloisCategory C],
CategoryTheory.Limits.HasPullbacks C
This theorem states that for any type `C` that forms a category (as indicated by `CategoryTheory.Category C`), if `C` is also a pre-Galois category (indicated by `CategoryTheory.PreGaloisCategory C`), then `C` has pullbacks. In mathematical terms, pullbacks are a certain type of limit in category theory. Specifically, given two morphisms `f : Z -> X` and `g : Z -> Y` in a category, a pullback is an object `P` along with two morphisms `p1 : P -> X` and `p2 : P -> Y` such that the diagram commutes (i.e., `f ∘ p1 = g ∘ p2`) and `P` is universal with respect to this property.
More concisely: In a pre-Galois category `C`, the presence of pullbacks is implied by the category structure and the pre-Galois property.
|