exactPairingOfFullyFaithful

Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.exactPairingOfFullyFaithful

Lean4

/-- Given a pair of objects which are sent by a fully faithful functor to a pair of objects
with an exact pairing, we get an exact pairing.
-/
def exactPairingOfFullyFaithful [F.Full] [F.Faithful] (X Y : C) [ExactPairing (F.obj X) (F.obj Y)] : ExactPairing X Y :=
  exactPairingOfFaithful F (F.preimage (δ F _ _ ≫ ε_ _ _ ≫ (ε F))) (F.preimage (η F ≫ η_ _ _ ≫ μ F _ _)) (by simp)
    (by simp)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru