Theorems · Theorem · combinatorics

Prefunctor.costar_conj_star

∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V)
  [inst_2 : Quiver.HasInvolutiveReverse U] [inst_3 : Quiver.HasInvolutiveReverse V] [φ.MapReverse] (u : U),
  φ.costar u = ⇑(Quiver.starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(Quiver.starEquivCostar u).symm

Defined in

Mathlib.Combinatorics.Quiver.Covering

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

QuiverQuiverQuiver.HasInvolutiveReverseQuiver.HasInvolutiveReversePrefunctor.MapReverse