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.isIso_liftToSubmodule: the factorization is an isomorphism when the morphism is injective on sections with image exactly N;
• TauCeti.SheafOfModules.Submodule.homOfLE, the inclusion of one submodule of a sheaf of modules into a larger one;
• SheafOfModules.Submodule.overIsoOfEq, the identification over V of two submodules with the same sections over every object above V.

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

theorem TauCeti.SheafOfModules.ι_val_app_injective {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ᵒᵖ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (N.ι.val.app U))

The inclusion of a submodule sheaf is injective on sections.

@[simp]

theorem TauCeti.SheafOfModules.range_ι_val_app {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ᵒᵖ) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (N.ι.app U)) = ↑(N.obj U)

The image of the inclusion on sections is the defining submodule.

theorem TauCeti.SheafOfModules.isIso_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) (hinj : ∀ (U : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.val.app U))) (hsurj : ∀ (U : Cᵒᵖ), ∀ s ∈ N.obj U, ∃ (t : ↑(P.val.obj U)), (CategoryTheory.ConcreteCategory.hom (φ.val.app U)) t = s) : CategoryTheory.IsIso (liftToSubmodule N φ hφ)

The factorization liftToSubmodule N φ hφ is an isomorphism when φ is injective on sections and every section of N is in the image of φ.

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✝

noncomputable def SheafOfModules.Submodule.overIsoOfEq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N₁ N₂ : M.Submodule) (V : C) (h : ∀ (W : C) (x : W ⟶ V), N₁.obj (Opposite.op W) = N₂.obj (Opposite.op W)) : N₁.toSheafOfModules.over V ≅ N₂.toSheafOfModules.over V

Two submodules of a sheaf of modules which have the same sections over every object above V give isomorphic sheaves of modules over V, compatibly with their inclusions (overIsoOfEq_hom_ι, overIsoOfEq_inv_ι).

Equations

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

instance SheafOfModules.Submodule.instMonoιOver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N : M.Submodule) (V : C) : CategoryTheory.Mono (Hom.over N.ι V)

The inclusion of a submodule remains a monomorphism after restricting to an object.

@[simp]

theorem SheafOfModules.Submodule.overIsoOfEq_hom_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N₁ N₂ : M.Submodule) (V : C) (h : ∀ (W : C) (x : W ⟶ V), N₁.obj (Opposite.op W) = N₂.obj (Opposite.op W)) : CategoryTheory.CategoryStruct.comp (N₁.overIsoOfEq N₂ V h).hom (Hom.over N₂.ι V) = Hom.over N₁.ι V

The isomorphism overIsoOfEq is compatible with the inclusions into M.

@[simp]

theorem SheafOfModules.Submodule.overIsoOfEq_hom_ι_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) (V : C) (h : ∀ (W : C) (x : W ⟶ V), N₁.obj (Opposite.op W) = N₂.obj (Opposite.op W)) {Z : SheafOfModules (R.over V)} (h✝ : M.over V ⟶ Z) : CategoryTheory.CategoryStruct.comp (N₁.overIsoOfEq N₂ V h).hom (CategoryTheory.CategoryStruct.comp (Hom.over N₂.ι V) h✝) = CategoryTheory.CategoryStruct.comp (Hom.over N₁.ι V) h✝

The isomorphism overIsoOfEq is compatible with the inclusions into M.

@[simp]

theorem SheafOfModules.Submodule.overIsoOfEq_inv_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (N₁ N₂ : M.Submodule) (V : C) (h : ∀ (W : C) (x : W ⟶ V), N₁.obj (Opposite.op W) = N₂.obj (Opposite.op W)) : CategoryTheory.CategoryStruct.comp (N₁.overIsoOfEq N₂ V h).inv (Hom.over N₁.ι V) = Hom.over N₂.ι V

The inverse of overIsoOfEq is compatible with the inclusions into M.

@[simp]

theorem SheafOfModules.Submodule.overIsoOfEq_inv_ι_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) (V : C) (h : ∀ (W : C) (x : W ⟶ V), N₁.obj (Opposite.op W) = N₂.obj (Opposite.op W)) {Z : SheafOfModules (R.over V)} (h✝ : M.over V ⟶ Z) : CategoryTheory.CategoryStruct.comp (N₁.overIsoOfEq N₂ V h).inv (CategoryTheory.CategoryStruct.comp (Hom.over N₁.ι V) h✝) = CategoryTheory.CategoryStruct.comp (Hom.over N₂.ι V) h✝

The inverse of overIsoOfEq is compatible with the inclusions into M.