IsHausdorff.haus
theorem IsHausdorff.haus :
∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
IsHausdorff I M → ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
The theorem `IsHausdorff.haus` states that for any commutative ring `R`, any ideal `I` of `R`, and any module `M` over `R` that is Hausdorff with respect to `I`, for every element `x` in `M`, if `x` is equivalent to zero modulo the nth power of `I` scaled by the top element of `R`, for all natural numbers `n`, then `x` is equal to zero. In simple terms, in a Hausdorff module over a commutative ring, any element that is arbitrarily close to zero in a certain sense is actually zero.
More concisely: In a commutative ring and its Hausdorff module, an element equivalent to zero under repeated powers of an ideal is actually zero.
|
Hausdorffification.lift_eq
theorem Hausdorffification.lift_eq :
∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N)
(g : Hausdorffification I M →ₗ[R] N), g ∘ₗ Hausdorffification.of I M = f → g = Hausdorffification.lift I f
The theorem `Hausdorffification.lift_eq` states that for a given commutative ring `R`, an ideal `I` in `R`, modules `M` and `N` over `R` with `N` being Hausdorff with respect to `I`, and given linear maps `f : M →ₗ[R] N` and `g : Hausdorffification I M →ₗ[R] N`, if the composition of `g` and the canonical map to the Hausdorffification of `M` with respect to `I` is equal to `f`, then `g` is equal to the lift of `f` to the Hausdorffification of `M`. In simpler terms, this theorem expresses the uniqueness of the function that extends `f` to the Hausdorffification of `M`.
More concisely: Given a commutative ring `R`, an ideal `I` in `R`, Hausdorff module `N` over `R`, modules `M` with `N` being Hausdorff with respect to `I`, linear maps `f : M → N` and `g : Hausdorffification I M → N`, if `g ∘ i_Hausdorff = f`, then `g = lift_eq f`.
|