Linear maps out of directed unions of submodules

This file gives the universal property of a directed union of submodules. A compatible family of linear maps on the members of a directed family glues to a linear map on any submodule of their supremum.

The construction TauCeti.Submodule.iSupLift is the linear analogue of Subalgebra.iSupLift. It uses Set.iUnionLift and the directedness of the family to prove that the local maps agree on overlaps.

Main declarations

• TauCeti.Submodule.iSupLift: glue compatible linear maps on a directed family of submodules.
• TauCeti.Submodule.iSupLift_inclusion and TauCeti.Submodule.iSupLift_of_mem: pointwise evaluation rules for the glued map.
• TauCeti.Submodule.iSupLift_mk: the glued map agrees with each prescribed map.
• TauCeti.Submodule.iSupLift_comp_inclusion: restricting the glued map recovers each prescribed map.
• TauCeti.Submodule.iSupLift_unique: the restriction property characterizes the glued map.

noncomputable def TauCeti.Submodule.iSupLift {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (K : ι → Submodule R M) (dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K) (f : (i : ι) → ↥(K i) →ₗ[R] P) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h) (T : Submodule R M) (hT : T ≤ iSup K) : ↥T →ₗ[R] P

Define a linear map on a submodule of a directed supremum by defining it compatibly on each member of the directed family.

Equations

• TauCeti.Submodule.iSupLift K dir f hf T hT = if hι : Nonempty ι then have x := hι; TauCeti.Submodule.iSupLiftNonempty✝ K dir f hf T hT else 0

@[simp]

theorem TauCeti.Submodule.iSupLift_mk {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {K : ι → Submodule R M} {dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₗ[R] P} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h} {T : Submodule R M} {hT : T ≤ iSup K} {i : ι} (m : ↥(K i)) (hm : ↑m ∈ T) : (iSupLift K dir f hf T hT) ⟨↑m, hm⟩ = (f i) m

The map glued on a directed supremum agrees with a prescribed map on each member of the family.

@[simp]

theorem TauCeti.Submodule.iSupLift_inclusion {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {K : ι → Submodule R M} {dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₗ[R] P} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h} {T : Submodule R M} {hT : T ≤ iSup K} {i : ι} (m : ↥(K i)) (h : K i ≤ T) : (iSupLift K dir f hf T hT) ((Submodule.inclusion h) m) = (f i) m

The map glued on a directed supremum agrees with a prescribed map after inclusion into its domain.

theorem TauCeti.Submodule.iSupLift_of_mem {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {K : ι → Submodule R M} {dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₗ[R] P} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h} {T : Submodule R M} {hT : T ≤ iSup K} {i : ι} (m : ↥T) (hm : ↑m ∈ K i) : (iSupLift K dir f hf T hT) m = (f i) ⟨↑m, hm⟩

Evaluate the map glued on a directed supremum at an element known to lie in one member of the family.

@[simp]

theorem TauCeti.Submodule.iSupLift_comp_inclusion {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {K : ι → Submodule R M} {dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₗ[R] P} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h} {T : Submodule R M} {hT : T ≤ iSup K} {i : ι} (h : K i ≤ T) : iSupLift K dir f hf T hT ∘ₗ Submodule.inclusion h = f i

Restricting the map glued on a directed supremum to a member of the family recovers the prescribed map.

theorem TauCeti.Submodule.iSupLift_unique {R : Type u} {M : Type v} {P : Type w} {ι : Type x} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] {K : ι → Submodule R M} {dir : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₗ[R] P} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = f j ∘ₗ Submodule.inclusion h} {T : Submodule R M} {hT : T ≤ iSup K} (g : ↥T →ₗ[R] P) (hg : ∀ (i : ι) (m : ↥(K i)) (hm : ↑m ∈ T), g ⟨↑m, hm⟩ = (f i) m) : g = iSupLift K dir f hf T hT

A linear map on a submodule of a directed supremum is determined by its values on the members of the directed family.