mathlib3 documentation

category_theory.elementwise

Use the elementwise attribute to create applied versions of lemmas. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Usually we would use @[elementwise] at the point of definition, however some early parts of the category theory library are imported by tactic.elementwise, so we need to add the attribute after the fact.

We now add some elementwise attributes to lemmas that were proved earlier.

source
@[simp]
theorem category_theory.is_iso.inv_hom_id_apply {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] [I_1 : category_theory.concrete_category C] (x : ↥Y) :
⇑f (⇑(category_theory.inv f) x) = x
source
@[simp]
theorem category_theory.iso.inv_hom_id_apply {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) [I : category_theory.concrete_category C] (x : ↥Y) :
⇑(self.hom) (⇑(self.inv) x) = x
source
@[simp]
theorem category_theory.is_iso.hom_inv_id_apply {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] [I_1 : category_theory.concrete_category C] (x : ↥X) :
⇑(category_theory.inv f) (⇑f x) = x
source
@[simp]
theorem category_theory.iso.hom_inv_id_apply {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) [I : category_theory.concrete_category C] (x : ↥X) :
⇑(self.inv) (⇑(self.hom) x) = x