Linear maps out of directed unions of finite subcomodules

This file specializes the universal property of a directed union of submodules to the finite subcomodules of a comodule. A compatible family of linear maps on the finite subcomodules glues to a linear map on the whole comodule as soon as every element lies in a finite subcomodule.

This is a prerequisite for the Tannakian reconstruction step in the ReductiveGroups roadmap: the components of a tensor automorphism on the finite subcomodules of the regular comodule must be assembled into one linear functional on the coordinate Hopf algebra.

Main declarations

• TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem: glue a compatible family under an explicit covering hypothesis.
• TauCeti.Subcomodule.finiteSubcomoduleLift: glue such a family when the coefficient coalgebra is free.
• TauCeti.Subcomodule.finiteSubcomoduleLift_apply: the glued map restricts to each member of the family.
• TauCeti.Subcomodule.finiteSubcomoduleLift_unique: the restriction property characterizes the glued map.

noncomputable def TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) : M →ₗ[R] P

Glue a compatible family of linear maps on the finite subcomodules of a comodule.

Compatibility is expressed along inclusions. The hypothesis hM says that the finite subcomodules cover M; it is supplied by exists_finite_subcomodule_mem whenever C is free as an R-module.

Equations

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

@[simp]

theorem TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem_apply {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (N : ↑finiteSubcomodules) (m : ↥↑N) : (finiteSubcomoduleLiftOfExistsMem hM f hf) ↑m = (f N) m

The map glued from finite subcomodules agrees with the prescribed map on each finite subcomodule.

@[simp]

theorem TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem_comp_subtype {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (N : ↑finiteSubcomodules) : finiteSubcomoduleLiftOfExistsMem hM f hf ∘ₗ (↑N).toSubmodule.subtype = f N

Restricting the map glued from finite subcomodules to one finite subcomodule recovers its prescribed map.

theorem TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem_unique {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] (hM : ∀ (m : M), ∃ (N : Subcomodule R C M), Module.Finite R ↥N.toSubmodule ∧ m ∈ N) (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (g : M →ₗ[R] P) (hg : ∀ (N : ↑finiteSubcomodules) (m : ↥↑N), g ↑m = (f N) m) : g = finiteSubcomoduleLiftOfExistsMem hM f hf

A linear map out of a comodule is determined by its restrictions to all finite subcomodules.

noncomputable def TauCeti.Subcomodule.finiteSubcomoduleLift {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] [Module.Free R C] (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) : M →ₗ[R] P

Glue a compatible family of linear maps on the finite subcomodules of a comodule whose coefficient coalgebra is free as a module.

Equations

• TauCeti.Subcomodule.finiteSubcomoduleLift f hf = TauCeti.Subcomodule.finiteSubcomoduleLiftOfExistsMem ⋯ f hf

@[simp]

theorem TauCeti.Subcomodule.finiteSubcomoduleLift_apply {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] [Module.Free R C] (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (N : ↑finiteSubcomodules) (m : ↥↑N) : (finiteSubcomoduleLift f hf) ↑m = (f N) m

The map glued from the finite subcomodules of a comodule over a free coalgebra agrees with the prescribed map on each finite subcomodule.

@[simp]

theorem TauCeti.Subcomodule.finiteSubcomoduleLift_comp_subtype {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] [Module.Free R C] (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (N : ↑finiteSubcomodules) : finiteSubcomoduleLift f hf ∘ₗ (↑N).toSubmodule.subtype = f N

Restricting the map glued from finite subcomodules over a free coefficient coalgebra to one finite subcomodule recovers its prescribed map.

theorem TauCeti.Subcomodule.finiteSubcomoduleLift_unique {R : Type u} {C : Type v} {M : Type w} {P : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid P] [Module R P] [Module.Free R C] (f : (N : ↑finiteSubcomodules) → ↥↑N →ₗ[R] P) (hf : ∀ (N Q : ↑finiteSubcomodules) (hNQ : ↑N ≤ ↑Q), f N = f Q ∘ₗ Submodule.inclusion hNQ) (g : M →ₗ[R] P) (hg : ∀ (N : ↑finiteSubcomodules) (m : ↥↑N), g ↑m = (f N) m) : g = finiteSubcomoduleLift f hf

A linear map out of a comodule over a free coefficient coalgebra is determined by its restrictions to the finite subcomodules.