CategoryTheory.Groupoid.inv_eq_inv
theorem CategoryTheory.Groupoid.inv_eq_inv :
∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.Groupoid.inv f = CategoryTheory.inv f
This theorem, `CategoryTheory.Groupoid.inv_eq_inv`, states that for any given category theory groupoid `C` of some type `u`, and any two objects `X` and `Y` in this groupoid, the inverse of a morphism `f` from `X` to `Y` in the groupoid context (given by `CategoryTheory.Groupoid.inv f`) is equal to the inverse of the same morphism `f` in the context of an isomorphism (given by `CategoryTheory.inv f`). In other words, the inverse morphism in a groupoid and the inverse of an isomorphism are the same entity when they are applied to the same morphism between the same objects in the groupoid.
More concisely: For any groupoid `C` and morphism `f` in `C` between objects `X` and `Y`, the inverse of `f` in the groupoid context equals the inverse of `f` as an isomorphism.
|
CategoryTheory.Groupoid.inv_comp
theorem CategoryTheory.Groupoid.inv_comp :
∀ {obj : Type u} [self : CategoryTheory.Groupoid obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y
The theorem `CategoryTheory.Groupoid.inv_comp` states that for any objects `X` and `Y` in a groupoid `obj`, and for any morphism `f` from `X` to `Y`, the composition of the inverse of `f` with `f` itself results in the identity morphism on `Y`. In mathematical terms, given a morphism `f: X ⟶ Y`, then `inv(f) ∘ f = id(Y)`, where `inv(f)` is the inverse of `f`, `∘` is the composition operation, and `id(Y)` is the identity morphism on `Y`.
More concisely: For any morphism `f` in a groupoid, the composition of its inverse with `f` equals the identity morphism on the target object of `f`.
|
CategoryTheory.Groupoid.comp_inv
theorem CategoryTheory.Groupoid.comp_inv :
∀ {obj : Type u} [self : CategoryTheory.Groupoid obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X
The theorem `CategoryTheory.Groupoid.comp_inv` states that for every object type `obj` in a groupoid `self`, and for any two objects `X` and `Y` of that type, if `f` is a morphism from `X` to `Y`, then the composition of `f` with its inverse `inv f` is equal to the identity morphism on `X`. In mathematical terms, this can be expressed as `f ∘ inv(f) = id_X`, where `∘` denotes composition of morphisms, `inv(f)` is the inverse of `f`, and `id_X` is the identity morphism on `X`. This is a fundamental property of groupoids in category theory.
More concisely: For any morphism `f` in a groupoid, `f ∘ inv(f) = id` where `inv(f)` is the inverse of `f` and `id` is the identity morphism on the source object of `f`.
|