Theorems · Theorem · category theory
CategoryTheory.Bicategory.conjugateEquiv_symm_id
∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
(adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁),
(CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id r₁) =
CategoryTheory.CategoryStruct.id l₁- Cited by
- 1 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Bicategory
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Equivstatement · cited by 8,337
- CategoryTheory.CategoryStruct.idstatement and proof · cited by 6,235
- Equiv.symmstatement · cited by 3,681
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- CategoryTheory.Bicategory.Adjunctionstatement and proof · cited by 83
- Equiv.symm_apply_eqproof · cited by 63
- CategoryTheory.Bicategory.conjugateEquivstatement and proof · cited by 41
- CategoryTheory.Bicategory.conjugateEquiv_idproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.conjugateEquiv_symm_commproof · cited by 0