CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext

theorem CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{u_5, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_6, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂} {R R' : Φ.RightResolution X₂} (x y : R.Hom R'), x.f = y.f → x = y

The theorem `CategoryTheory.LocalizerMorphism.RightResolution.Hom.ext` states that for any two categories `C₁` and `C₂` with corresponding morphism properties `W₁` and `W₂`, a localizer morphism `Φ` between `W₁` and `W₂`, and an object `X₂` in `C₂`, for any two right resolutions `R` and `R'` of `Φ` and `X₂`, if two morphisms `x` and `y` from `R` to `R'` have the same underlying function (i.e., `x.f = y.f`), then `x` and `y` are the same morphism (i.e., `x = y`). This theorem therefore guarantees the uniqueness of morphisms in the context of category theory when they have the same underlying function.

More concisely: Given categories `C₁`, `C₂`, morphism properties `W₁` and `W₂`, a localizer morphism `Φ` between `W₁` and `W₂`, and objects `X₂` in `C₂`, if `R` and `R'` are right resolutions of `Φ` and `X₂`, then morphisms `x` and `y` in `R` with equal underlying functions `x.f = y.f` are equal `x = y`.