Fixed-target arrow extension by categorical denominator clearing #
Suppose an R-linear functor has lifts of target objects, its map on Homs into a fixed
object is a localization, and each denominator acts invertibly on the image of a lifted
source object. A fraction representing a target arrow can then be cleared by changing
the source isomorphism. No full faithfulness, exactness, or geometric localization is
asserted here.
theorem
CategoryTheory.Subobject.fixedTargetArrowExtension_of_localizedHom
(R : Type w)
[CommRing R]
(S : Submonoid R)
{C : Type u₁}
[Category.{v₁, u₁} C]
[Preadditive C]
[Linear R C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[Preadditive D]
[Linear R D]
(F : Functor C D)
[F.Additive]
[Functor.Linear R F]
(X : C)
(hObj : ∀ (Z : D), ∃ (Y : C), Nonempty (Z ≅ F.obj Y))
(hHom : ∀ (Y : C), IsLocalizedModule S (Functor.mapLinearMap R F))
(hIso : ∀ (Y : C) (s : ↥S), IsIso (↑s • CategoryStruct.id (F.obj Y)))
:
Clear a denominator in a morphism into F.obj X by absorbing its action into
the isomorphism from a target source object to the image of a source object.
Only the Hom-localization maps with fixed codomain X are needed.