Units from automorphisms of the rank-one free module

An automorphism of a ring as a module over itself sends one to a unit. Consequently, the scalar comparing the images of one under two isomorphisms is a unit as well.

A natural number e kills a module M exactly when the endomorphism e • 𝟙 M vanishes (ModuleCat.nsmul_id_eq_zero_iff).

theorem ModuleCat.isUnit_apply_one_of_isIso {R : Type u} [Ring R] (f : ↧R ⟶ ↧R) [CategoryTheory.IsIso f] : IsUnit ((CategoryTheory.ConcreteCategory.hom f) 1)

An automorphism of the rank-one free module sends one to a unit.

theorem ModuleCat.isUnit_of_apply_one_eq_smul {R : Type u} [Ring R] {M : ModuleCat R} (f g : ↧R ⟶ M) [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] {a : R} (h : (CategoryTheory.ConcreteCategory.hom g) 1 = a • (CategoryTheory.ConcreteCategory.hom f) 1) : IsUnit a

The scalar comparing the images of one under two module isomorphisms is a unit.

theorem ModuleCat.nsmul_id_eq_zero_iff {R : Type u} [Ring R] {M : ModuleCat R} {e : ℕ} : e • CategoryTheory.CategoryStruct.id M = 0 ↔ ∀ (x : ↑M), e • x = 0

A natural number e kills a module M, in the sense that e • 𝟙 M = 0, exactly when e • x = 0 for every element x of M.