ModuleCat.ext
theorem ModuleCat.ext :
∀ (R : Type u) [inst : Ring R] {M N : ModuleCat R} {f₁ f₂ : M ⟶ N}, (∀ (x : ↑M), f₁ x = f₂ x) → f₁ = f₂
This theorem states that given a type `R` that forms a ring, for any two modules `M` and `N` over `R` and any two morphisms `f₁` and `f₂` from `M` to `N`, if `f₁` and `f₂` are equal for all elements of `M` then `f₁` is equal to `f₂`. In other words, two morphisms between two modules over a ring are identical if they agree on every point in the domain module.
More concisely: If two morphisms between two modules over a ring agree on all elements of the domain module, then they are equal.
|
ModuleCat.coe_comp
theorem ModuleCat.coe_comp :
∀ {R : Type u} [inst : Ring R] {M N U : ModuleCat R} (f : M ⟶ N) (g : N ⟶ U),
⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
The theorem `ModuleCat.coe_comp` states that for any type `R` with a ring structure, and for any three `R`-modules `M`, `N`, and `U`, the composition of two morphisms `f : M ⟶ N` and `g : N ⟶ U` (in the category of `R`-modules) is equal to the composition of the corresponding functions. In other words, if we apply the coercion (`⇑`) to the composition of `f` and `g`, we get the same result as if we first apply `⇑` to `f` and `g` separately and then compose them as regular functions. This theorem justifies working with elements of modules in the same way we work with functions when it comes to composition.
More concisely: For any ring `R` and `R`-module morphisms `f : M ⟶ N` and `g : N ⟶ U`, `⇑(g ∘ f) = ⇑g ∘ ⇑f` in the category of `R`-modules.
|