Quiver.reverse_reverse
theorem Quiver.reverse_reverse :
∀ {V : Type u_2} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (f : a ⟶ b),
Quiver.reverse (Quiver.reverse f) = f
The theorem `Quiver.reverse_reverse` states that for any type `V` that has a structure of a `Quiver` and an involution on the reversal operation, given any two objects `a` and `b` in this `Quiver` and a morphism `f` from `a` to `b`, applying the `reverse` operation twice on the morphism `f` (which flips its direction) returns the original morphism `f`. In other words, reversing the direction of a reversed morphism brings it back to its original form. This theorem essentially encapsulates the mathematical property that reversal is an involution (a function that is its own inverse).
More concisely: For any object pair `a` and `b` in a quiver `V` with an involution on reversal, and any morphism `f` from `a` to `b`, we have `reverse (reverse f) = f`.
|
Prefunctor.MapReverse.map_reverse'
theorem Prefunctor.MapReverse.map_reverse' :
∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver.HasReverse U]
[inst_3 : Quiver.HasReverse V] {φ : U ⥤q V} [self : φ.MapReverse] {u v : U} (e : u ⟶ v),
φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)
The theorem `Prefunctor.MapReverse.map_reverse'` states that for any two types `U` and `V` that have a Quiver structure and can be reversed (i.e., arrows between elements can be reversed), if `φ` is a functor from `U` to `V` and it has the property `MapReverse`, then for any two elements `u` and `v` of `U` and an arrow `e` from `u` to `v`, the result of first reversing `e` and then applying the functor `φ` is the same as the result of first applying the functor `φ` to `e` and then reversing. In other words, reversing and then mapping is the same as mapping and then reversing.
More concisely: For any Quiver structures `U` and `V` and a functor `φ` from `U` to `V` with the `MapReverse` property, reversing an arrow `e` from `u` to `v` in `U` and applying `φ` is equivalent to applying `φ` to `e` and then reversing it in `V`.
|
Quiver.HasInvolutiveReverse.inv'
theorem Quiver.HasInvolutiveReverse.inv' :
∀ {V : Type u_2} [inst : Quiver V] [self : Quiver.HasInvolutiveReverse V] {a b : V} (f : a ⟶ b),
Quiver.reverse (Quiver.reverse f) = f
This theorem states that the `reverse` operation, as defined in the context of Quivers, is involutive. In other words, for all types `V` that have a Quiver structure and an InvolutiveReverse structure, and for all objects `a` and `b` of type `V`, if you take an arrow `f` from `a` to `b` and reverse it twice using the `Quiver.reverse` operation, you get back the original arrow `f`. This property is equivalent to saying that the double application of the reverse operation is the identity operation on the set of arrows from `a` to `b`.
More concisely: For any type `V` with Quiver and InvolutiveReverse structures, the `Quiver.reverse` operation is involutive on arrows, i.e., `Quiver.reverse (Quiver.reverse f) = f` for all arrows `f` from objects in `V`.
|
Quiver.Symmetrify.lift_unique
theorem Quiver.Symmetrify.lift_unique :
∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [inst_2 : Quiver.HasReverse V']
(φ : V ⥤q V') (Φ : Quiver.Symmetrify V ⥤q V'),
Quiver.Symmetrify.of.comp Φ = φ →
(∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) →
Φ = Quiver.Symmetrify.lift φ
The theorem `Quiver.Symmetrify.lift_unique` states that for any two types `V` and `V'` that form quivers (directed graphs) where `V'` also has a reversible arrow operation, a given prefunctor `φ` from `V` to `V'`, and another prefunctor `Φ` from the symmetrification of `V` to `V'`, if the composition of `Quiver.Symmetrify.of` and `Φ` equals `φ` and `Φ` preserves the reverse of any arrow in the symmetrified `V`, then `Φ` must be equivalent to the lift of `φ` via `Quiver.Symmetrify.lift`. In other words, the `lift φ` is the unique prefunctor that extends `φ` and preserves the operation of reversing arrows.
More concisely: Given quivers V and V' with reversible arrows in V', a prefunctor φ from V to V', and a prefunctor Φ from the symmetrification of V to V' preserving the reverse of arrows and such that Quiver.Symmetrify.of ∘ Φ = φ, then Φ is equivalent to the lift of φ via Quiver.Symmetrify.lift.
|