ι_gluedIso_inv — Mathlib

English

The image of ι under F commutes with the glued iso in GluedData: F.map(ι i) ≫ gluedIso.hom = mapGlueData.ι i.

Русский

Изображение ι через F commuting с gluedIso: F.map(ι i) ⋅ gluedIso.hom = mapGlueData.ι i.

LaTeX

$$$F.map(\\iota_i) \\circ (D.gluedIso F).hom = (D.mapGlueData F).\\iota_i$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_gluedIso_inv (i : D.J) : (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i) := by
  rw [Iso.comp_inv_eq, ι_gluedIso_hom]

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