English
Opposite of RightFractionRel yields LeftFractionRel via unop.
Русский
Обратное отражение RightFractionRel даёт LeftFractionRel через unop.
LaTeX
$$$LeftFractionRel(z_1^{unop}, z_2^{unop}) \Rightarrow RightFractionRel(z_1,z_2)$$$
Lean4
/-- A `MorphismProperty` in `W.Localization` is satisfied by all
morphisms in the localized category if it contains the image of the
morphisms in the original category, the inverses of the morphisms
in `W` and if it is stable under composition -/
theorem morphismProperty_is_top (P : MorphismProperty W.Localization) [P.IsStableUnderComposition]
(hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) (hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)) : P = ⊤ :=
by
funext X Y f
ext
constructor
· intro
apply MorphismProperty.top_apply
· intro
let G : _ ⥤ W.Localization := Quotient.functor _
haveI : G.Full := Quotient.full_functor _
suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
by
rcases X with ⟨⟨X⟩⟩
rcases Y with ⟨⟨Y⟩⟩
simpa only [Functor.map_preimage] using this _ _ (G.preimage f)
intro X₁ X₂ p
induction p with
| nil => simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
| @cons X₂ X₃ p g hp =>
let p' : X₁ ⟶ X₂ := p
rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
refine P.comp_mem _ _ hp ?_
rcases g with (g | ⟨g, hg⟩)
· apply hP₁
· apply hP₂
