Factoring a morphism through a submodule of a (pre)sheaf of modules

Mathlib's PresheafOfModules.Submodule and SheafOfModules.Submodule package a submodule of a (pre)sheaf of modules together with the inclusion N.ι of the associated (pre)sheaf of modules. This file supplies the missing universal property of that inclusion: a morphism whose sections all land in N factors through N, uniquely because N.ι is a monomorphism.

Main declarations

• TauCeti.PresheafOfModules.liftToSubmodule and TauCeti.SheafOfModules.liftToSubmodule, the factorization itself, with liftToSubmodule_ι recording that it does factor the given morphism;
• TauCeti.SheafOfModules.Submodule.homOfLE, the inclusion of one submodule of a sheaf of modules into a larger one.

No formalization is vendored; the constructions are AddMonoidHom.codRestrict applied section by section, assembled by Mathlib's PresheafOfModules.homMk.

noncomputable def TauCeti.PresheafOfModules.liftToSubmodule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M P : PresheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.app U)) s ∈ N.obj U) : P ⟶ N.toPresheafOfModules

A morphism of presheaves of modules all of whose sections lie in a submodule N of the target factors through the presheaf of modules attached to N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PresheafOfModules.liftToSubmodule_app_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M P : PresheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.app U)) s ∈ N.obj U) (U : Cᵒᵖ) (s : ↑(P.obj U)) : ↑((CategoryTheory.ConcreteCategory.hom ((liftToSubmodule N φ hφ).app U)) s) = (CategoryTheory.ConcreteCategory.hom (φ.app U)) s

@[simp]

theorem TauCeti.PresheafOfModules.liftToSubmodule_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M P : PresheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.app U)) s ∈ N.obj U) : CategoryTheory.CategoryStruct.comp (liftToSubmodule N φ hφ) N.ι = φ

@[simp]

theorem TauCeti.PresheafOfModules.liftToSubmodule_ι_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M P : PresheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.app U)) s ∈ N.obj U) {Z : PresheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftToSubmodule N φ hφ) (CategoryTheory.CategoryStruct.comp N.ι h) = CategoryTheory.CategoryStruct.comp φ h

theorem TauCeti.PresheafOfModules.ι_app_mem {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (N : M.Submodule) (U : Cᵒᵖ) (s : ↑(N.toPresheafOfModules.obj U)) : (CategoryTheory.ConcreteCategory.hom (N.ι.app U)) s ∈ N.obj U

noncomputable def TauCeti.SheafOfModules.liftToSubmodule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M P : SheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.val.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) s ∈ N.obj U) : P ⟶ N.toSheafOfModules

A morphism of sheaves of modules all of whose sections lie in a submodule N of the target factors through the sheaf of modules attached to N.

Equations

• TauCeti.SheafOfModules.liftToSubmodule N φ hφ = { val := TauCeti.PresheafOfModules.liftToSubmodule N.toSubmodule φ.val hφ }

@[simp]

theorem TauCeti.SheafOfModules.liftToSubmodule_val_app_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M P : SheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.val.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) s ∈ N.obj U) (U : Cᵒᵖ) (s : ↑(P.val.obj U)) : ↑((CategoryTheory.ConcreteCategory.hom ((liftToSubmodule N φ hφ).val.app U)) s) = (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) s

@[simp]

theorem TauCeti.SheafOfModules.liftToSubmodule_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M P : SheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.val.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) s ∈ N.obj U) : CategoryTheory.CategoryStruct.comp (liftToSubmodule N φ hφ) N.ι = φ

@[simp]

theorem TauCeti.SheafOfModules.liftToSubmodule_ι_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M P : SheafOfModules R} (N : M.Submodule) (φ : P ⟶ M) (hφ : ∀ (U : Cᵒᵖ) (s : ↑(P.val.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) s ∈ N.obj U) {Z : SheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftToSubmodule N φ hφ) (CategoryTheory.CategoryStruct.comp N.ι h) = CategoryTheory.CategoryStruct.comp φ h

theorem TauCeti.SheafOfModules.ι_val_app_mem {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) (U : Cᵒᵖ) (s : ↑(N.toSheafOfModules.val.obj U)) : (CategoryTheory.ConcreteCategory.hom (N.ι.val.app U)) s ∈ N.obj U

noncomputable def TauCeti.SheafOfModules.Submodule.homOfLE {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} (h : N₁.toSubmodule ≤ N₂.toSubmodule) : N₁.toSheafOfModules ⟶ N₂.toSheafOfModules

The inclusion of a submodule of a sheaf of modules into a larger one. The hypothesis is stated for the underlying submodules of the presheaf of modules, which is what SheafOfModules.Submodule.le_iff says the order on submodules of a sheaf of modules is.

Equations

• TauCeti.SheafOfModules.Submodule.homOfLE h = { val := PresheafOfModules.Submodule.homOfLE h }

@[simp]

theorem TauCeti.SheafOfModules.Submodule.homOfLE_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} (h : N₁.toSubmodule ≤ N₂.toSubmodule) : CategoryTheory.CategoryStruct.comp (homOfLE h) N₂.ι = N₁.ι

@[simp]

theorem TauCeti.SheafOfModules.Submodule.homOfLE_ι_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N₁ N₂ : M.Submodule} (h : N₁.toSubmodule ≤ N₂.toSubmodule) {Z : SheafOfModules R} (h✝ : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfLE h) (CategoryTheory.CategoryStruct.comp N₂.ι h✝) = CategoryTheory.CategoryStruct.comp N₁.ι h✝