w' — Mathlib · SciLib

English

Extensionality principle: two morphisms between pullbacks are equal if their fst and snd components are equal respectively.

Русский

Принцип экстенсиональности: два морфизма между pullback равны, если их компоненты fst и snd совпадают по очереди.

LaTeX

$$$ \forall x,y:\ F \loop G,\; (f,g): x\to y, f.fst = g.fst \land f.snd = g.snd \Rightarrow f = g$$$

Lean4

/-- Naturality square for morphisms in the inverse direction. -/
@[reassoc (attr := simp)]
theorem w' {x y : F ⊡ G} (f : x ⟶ y) : G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst := by
  rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]

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