English
The counit, under the inverse-image of isomorphisms along G, yields an isomorphism in the functor category setting.
Русский
Кауниут, рассматриваемый через обратное изображение изоморфизмов вдоль G, образует изоморфизм в категориальной категории функторов.
LaTeX
$$$((\mathrm{isomorphisms}(C_2)).inverseImage G).\mathrm{functorCategory} C_1\ adj.counit$$$
Lean4
theorem neg'_eq (f : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction X Y) (hφ : f = φ.map L (inverts L W)) :
neg' W f = φ.neg.map L (inverts L W) :=
by
obtain ⟨φ₀, rfl, hφ₀⟩ :
∃ (φ₀ : W.LeftFraction X Y) (_ : f = φ₀.map L (inverts L W)), neg' W f = φ₀.neg.map L (inverts L W) :=
⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩
rw [MorphismProperty.LeftFraction.map_eq_iff] at hφ
obtain ⟨Y', t₁, t₂, hst, hft, ht⟩ := hφ
have := inverts L W _ ht
rw [← cancel_mono (L.map (φ₀.s ≫ t₁))]
nth_rw 1 [L.map_comp]
rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp, LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ←
L.map_comp, neg_comp, neg_comp, hft]
