CategoryTheory.Subgroupoid.mem_objs_of_src
theorem CategoryTheory.Subgroupoid.mem_objs_of_src :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {c d : C} {f : c ⟶ d},
f ∈ S.arrows c d → c ∈ S.objs
This theorem states that for any category `C` that is also a groupoid, any subgroupoid `S` of `C`, and any arrows `f` from `c` to `d` in `C`, if `f` is an element of the arrows of `S` from `c` to `d`, then `c` is an element of the set of objects in `S` that have nontrivial isotropy. Here, isotropy refers to the symmetry of an object - in this case, the object `c` has nontrivial isotropy if there is at least one arrow (or morphism) in `S` that begins and ends at `c`.
More concisely: In a groupoid `C`, if `S` is a subgroupoid and `f` is an arrow from object `c` to `d` in `S`, then `c` belongs to the set of objects in `S` having nontrivial isotropy.
|
Mathlib.CategoryTheory.Groupoid.Subgroupoid._auxLemma.2
theorem Mathlib.CategoryTheory.Groupoid.Subgroupoid._auxLemma.2 :
∀ {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'}, (⟨a, h⟩ = ⟨a', h'⟩) = (a = a')
This theorem states that for any sort `α`, any predicate `p` over `α`, any two elements `a` and `a'` of `α` such that `p` holds for `a` and `a'` respectively, the equality of the two pairs `{ val := a, property := h }` and `{ val := a', property := h' }` (constructed with the elements and their properties) is the same as the equality of `a` and `a'`. Simply put, two such pairs are equal if and only if the elements they are constructed with are equal, irrespective of the properties.
More concisely: Given any sort `α`, predicate `p` over `α`, and elements `a` and `a'` of `α` such that `p(a)` and `p(a')` hold, the pairs `{val := a, property := h}` and `{val := a', property := h'}` are equal if and only if `a` and `a'` are equal.
|
Mathlib.CategoryTheory.Groupoid.Subgroupoid._auxLemma.16
theorem Mathlib.CategoryTheory.Groupoid.Subgroupoid._auxLemma.16 :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (D : Set C) {c d : C} {f : c ⟶ d},
(f ∈ (CategoryTheory.Subgroupoid.full D).arrows c d) = (c ∈ D ∧ d ∈ D)
This theorem states that for any type `C` that forms a groupoid, given a set `D` of `C`, and any morphism `f` from an object `c` to an object `d` in `C`, the morphism `f` is an arrow in the subgroupoid fully generated by `D` if and only if both `c` and `d` belong to `D`. In other words, the morphism `f` is part of the subgroupoid induced by `D` exactly when the objects `c` and `d` are elements of `D`.
More concisely: For any groupoid `C` and subset `D` of `C`, a morphism `f` from an object `c` to an object `d` in `C` belongs to the subgroupoid fully generated by `D` if and only if both `c` and `d` are elements of `D`.
|
CategoryTheory.Subgroupoid.le_iff
theorem CategoryTheory.Subgroupoid.le_iff :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S T : CategoryTheory.Subgroupoid C),
S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
This theorem is about the relation between two sub-groupoids in category theory. Given two sub-groupoids `S` and `T` of a groupoid `C`, this theorem states that `S` is less than or equal to `T` if and only if for all objects `c` and `d` in `C`, the set of arrows (or morphisms) in `S` from `c` to `d` is a subset of the set of arrows in `T` from `c` to `d`.
More concisely: Given sub-groupoids `S` and `T` of a groupoid `C`, `S` is included in `T` if and only if for all objects `c` and `d` in `C`, the set of arrows from `c` to `d` in `S` is a subset of the set of arrows from `c` to `d` in `T`.
|
CategoryTheory.Subgroupoid.ext
theorem CategoryTheory.Subgroupoid.ext :
∀ {C : Type u} {inst : CategoryTheory.Groupoid C} (x y : CategoryTheory.Subgroupoid C),
x.arrows = y.arrows → x = y
This theorem states that within the context of a groupoid `C` of a certain type `u`, for any two subgroupoids `x` and `y` of `C`, if the set of morphisms (arrows) in `x` is equal to the set of morphisms in `y`, then `x` and `y` are the same subgroupoid. In other words, two subgroupoids of a groupoid are identical if they have the same morphisms.
More concisely: In a groupoid `C` of type `u`, two subgroupoids `x` and `y` are equal if and only if they have the same set of morphisms.
|
CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy
theorem CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
∀ c ∈ S.objs, CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
This theorem states that for any given type `C` that forms a groupoid (as indicated by the presence of an instance of `CategoryTheory.Groupoid C`), and any subgroupoid `S` of this groupoid, if an object `c` is part of the set of vertices of the subgroupoid `S` on which `S` has non-trivial isotropy (meaning that there exists at least one morphism in `S` that starts and ends at `c`), then the identity morphism on `c` (which is a morphism from `c` to itself) is also in this set of morphisms in `S` that start and end at `c`.
In mathematical terms, it says that if a vertex has non-trivial isotropy in a subgroupoid (i.e., there is at least one morphism in the subgroupoid that loops back to the vertex), then the identity morphism on that vertex belongs to the set of morphisms of the subgroupoid from the vertex to itself.
More concisely: If a vertex `c` in a groupoid `C` has non-trivial isotropy in a subgroupoid `S`, then the identity morphism on `c` is in `S`.
|
CategoryTheory.Subgroupoid.galoisConnection_map_comap
theorem CategoryTheory.Subgroupoid.galoisConnection_map_comap :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
(φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
GaloisConnection (CategoryTheory.Subgroupoid.map φ hφ) (CategoryTheory.Subgroupoid.comap φ)
The theorem `CategoryTheory.Subgroupoid.galoisConnection_map_comap` states that for any types `C` and `D`, which are groupoids, and a functor `φ` from `C` to `D` such that `φ.obj` is an injective function, there exists a Galois connection between the map of subgroupoids induced by `φ` and the preimage of subgroupoids under `φ`. In other words, for any subgroupoid `S` of `C` and `T` of `D`, `S` is less than or equal to the preimage of `T` under `φ` if and only if the image of `S` under `φ` is less than or equal to `T`. This theorem is a fundamental result in the theory of groupoids in category theory, establishing a relationship between mappings and preimages of subgroupoids under functors.
More concisely: For injective functors φ from groupoids C and D, the map of subgroupoids induced by φ and the preimage of subgroupoids under φ form a Galois connection.
|