equivalenceSingleObjInverse — Mathlib

English

Restating the inverse equivalence: it is the inverse of the main equivalence between Mat R and Mat_(SingleObj (R^op)).

Русский

Повторное определение обратной эквивалентности: это обратная эквивалентность между Mat R и Mat_(SingleObj (R^op)).

LaTeX

$$$\mathrm{equivalenceSingleObjInverse}(R)$ is defined as the inverse of $\mathrm{equivalenceSingleObj}(R)$$$

Lean4

/-- Auxiliary definition for `CategoryTheory.Mat.equivalenceSingleObj`. -/
@[simps]
def equivalenceSingleObjInverse : Mat_ (SingleObj Rᵐᵒᵖ) ⥤ Mat R
    where
  obj X := FintypeCat.of X.ι
  map f i j := MulOpposite.unop (f i j)
  map_id
    X := by
    ext
    simp only [Mat_.id_def, id_def]
    split_ifs <;> rfl
  map_comp f
    g := by
    -- Porting note: this proof was automatic in mathlib3

    ext
    simp only [Mat_.comp_apply, comp_apply]
    apply Finset.unop_sum

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