Corestriction of subcomodules

Corestriction of a comodule along a coalgebra morphism preserves every subcomodule and its underlying submodule. When the coalgebra morphism is an equivalence, this gives an order isomorphism between the subcomodule lattices before and after corestriction.

This is Layer 1 infrastructure for the reductive-groups roadmap: changing coordinate coalgebras must preserve the invariant subspaces of their comodules.

Main declarations

• TauCeti.Subcomodule.corestrict: corestrict a subcomodule along a coalgebra morphism.
• TauCeti.Subcomodule.corestrictSymm: recover a subcomodule before corestriction along a coalgebra equivalence.
• TauCeti.Subcomodule.corestrictOrderIso: the carrier-preserving order isomorphism induced by a coalgebra equivalence.
• TauCeti.Subcomodule.isSimpleOrder_of_corestrict_eq_ofWeights: distinct one-dimensional weights connected by subcomodule-preserving involutions give a simple comodule.
• TauCeti.Subcomodule.weightComponent_mem_of_corestrict_eq_ofWeights: restriction to a diagonal comodule extracts entire weight components, including repeated weights.
• TauCeti.Subcomodule.single_smul_mem_of_corestrict_eq_ofWeights: restriction to distinct one-dimensional weights extracts each scaled coordinate vector of a subcomodule vector.
• TauCeti.Subcomodule.toSubmodule_eq_span_of_corestrict_eq_ofWeights: distinct one-dimensional weights make each subcomodule the span of its contained coordinate vectors.
• TauCeti.Subcomodule.ofCorestrictOfSplit and corestrictOrderIsoOfSplit: recovery and order correspondence given a linear retraction over a commutative semiring.
• TauCeti.Subcomodule.map_id_coact_coe_eq_tmul_one: a vector of a subcomodule fixed by the corestricted coaction is fixed by the corestricted coaction of the ambient comodule.

References

• M. Sweedler, Hopf Algebras, Chapter 2.

def TauCeti.Subcomodule.corestrict {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (W : Subcomodule R C M) : Subcomodule R D M

Corestriction along a coalgebra morphism preserves a subcomodule and its carrier.

Equations

• TauCeti.Subcomodule.corestrict f W = TauCeti.Subcomodule.ofSubmodule W.carrier ⋯

@[simp]

theorem TauCeti.Subcomodule.corestrict_toSubmodule {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (W : Subcomodule R C M) : (corestrict f W).toSubmodule = W.toSubmodule

Corestriction of a subcomodule does not change its underlying submodule.

@[simp]

theorem TauCeti.Subcomodule.mem_corestrict {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (W : Subcomodule R C M) (m : M) : m ∈ corestrict f W ↔ m ∈ W

Membership is unchanged by corestriction of a subcomodule.

def TauCeti.Subcomodule.corestrictSymm {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) (W : Subcomodule R D M) : Subcomodule R C M

Pull a subcomodule of a corestricted comodule back along a coalgebra equivalence.

Equations

• TauCeti.Subcomodule.corestrictSymm e W = TauCeti.Subcomodule.ofSubmodule W.carrier ⋯

@[simp]

theorem TauCeti.Subcomodule.corestrictSymm_toSubmodule {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) (W : Subcomodule R D M) : (corestrictSymm e W).toSubmodule = W.toSubmodule

Pulling a subcomodule back from a corestriction preserves its underlying submodule.

@[simp]

theorem TauCeti.Subcomodule.mem_corestrictSymm {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) (W : Subcomodule R D M) (m : M) : m ∈ corestrictSymm e W ↔ m ∈ W

Membership is unchanged when pulling a subcomodule back from a corestriction.

def TauCeti.Subcomodule.corestrictOrderIso {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) : Subcomodule R C M ≃o Subcomodule R D M

A coalgebra equivalence identifies the subcomodules of a comodule with those of its corestriction, without changing their underlying submodules.

Equations

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

@[simp]

theorem TauCeti.Subcomodule.corestrictOrderIso_apply {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) (W : Subcomodule R C M) : (corestrictOrderIso e) W = corestrict e.toCoalgHom W

The forward order correspondence is corestriction.

@[simp]

theorem TauCeti.Subcomodule.corestrictOrderIso_symm_apply {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (e : C ≃ₗc[R] D) (W : Subcomodule R D M) : (corestrictOrderIso e).symm W = corestrictSymm e W

The inverse order correspondence is pullback from the corestriction.

theorem TauCeti.Subcomodule.weightComponent_mem_of_corestrict_eq_ofWeights {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {G : Type w} {I : Type x} [Finite I] [DecidableEq G] [Comodule R C (I → R)] (f : C →ₗc[R] MonoidAlgebra R G) (wt : I → G) (hcomodule : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun R I) wt) (N : Subcomodule R C (I → R)) {v : I → R} (hv : v ∈ N) (g : G) : (fun (a : I) => if wt a = g then v a else 0) ∈ N

Restriction to a diagonal weight comodule extracts the entire component of each weight, without requiring the weights to be distinct.

theorem TauCeti.Subcomodule.single_smul_mem_of_corestrict_eq_ofWeights {H : Type v} [AddCommGroup H] {G : Type w} {I : Type x} [Finite I] [DecidableEq I] {k : Type u} [CommRing k] [Module k H] [Coalgebra k H] [Comodule k H (I → k)] (f : H →ₗc[k] MonoidAlgebra k G) (wt : I → G) (hwt : Function.Injective wt) (hcomodule : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k I) wt) (N : Subcomodule k H (I → k)) {v : I → k} (hv : v ∈ N) (a : I) : v a • Pi.single a 1 ∈ N

Restriction to distinct one-dimensional weights extracts every scaled coordinate vector of a vector in a subcomodule.

theorem TauCeti.Subcomodule.toSubmodule_eq_span_of_corestrict_eq_ofWeights {H : Type v} [AddCommGroup H] {G : Type w} {I : Type x} [Finite I] [DecidableEq I] {k : Type u} [Field k] [Module k H] [Coalgebra k H] [Comodule k H (I → k)] (f : H →ₗc[k] MonoidAlgebra k G) (wt : I → G) (hwt : Function.Injective wt) (hcomodule : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k I) wt) (N : Subcomodule k H (I → k)) : N.toSubmodule = Submodule.span k (⇑(Pi.basisFun k I) '' {a : I | Pi.single a 1 ∈ N})

If corestriction separates distinct one-dimensional weights, every subcomodule is spanned by the coordinate vectors it contains.

theorem TauCeti.Subcomodule.isSimpleOrder_of_corestrict_eq_ofWeights {H : Type v} [AddCommGroup H] {G : Type w} {I : Type x} [Finite I] [DecidableEq I] {k : Type u} [Field k] [Module k H] [Coalgebra k H] [Comodule k H (I → k)] (f : H →ₗc[k] MonoidAlgebra k G) (wt : I → G) (hwt : Function.Injective wt) (hcomodule : Comodule.Corestrict f = Comodule.ofWeights (Pi.basisFun k I) wt) {J : Type u_1} (reflect : J → I → I) (hinvolutive : ∀ (j : J), Function.Involutive (reflect j)) (hreflect : ∀ (N : Subcomodule k H (I → k)) (a : I) (j : J), Pi.single a 1 ∈ N → Pi.single (reflect j a) 1 ∈ N) (base : I) (hconnected : ∀ (a : I), ∃ (l : List J), List.foldl (fun (b : I) (j : J) => reflect j b) base l = a) : IsSimpleOrder (Subcomodule k H (I → k))

A comodule with distinct one-dimensional weights and a connected weight graph is simple. The graph edges are supplied as involutions of the basis indices which preserve membership of basis vectors in every subcomodule. This isolates the type-independent argument used for minuscule standard comodules: restriction to the torus extracts a coordinate, and connected root moves propagate that coordinate basis vector to the whole basis.

theorem TauCeti.Subcomodule.map_id_coact_coe_eq_tmul_one {R : Type u} [CommSemiring R] {C : Type v} {D : Type w} [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid D] [Module R D] [Coalgebra R D] [One D] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] (f : C →ₗc[R] D) (W : Subcomodule R C M) {n : ↥W} (hn : (TensorProduct.map LinearMap.id f.toLinearMap) (Comodule.coact n) = n ⊗ₜ[R] 1) : (TensorProduct.map LinearMap.id f.toLinearMap) (Comodule.coact ↑n) = ↑n ⊗ₜ[R] 1

A vector of a subcomodule that the corestricted coaction fixes is fixed by the corestricted coaction of the ambient comodule.

This is the corestricted analogue of TauCeti.Subcomodule.coact_coe_eq_tmul_one; the coalgebra morphism is spelled out rather than installed as a comodule instance, so that both sides read in the ambient coalgebra C.

def TauCeti.Subcomodule.ofCorestrictOfSplit {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k D V) : Subcomodule k C V

A linear retraction of a coalgebra morphism recovers every subcomodule of the corestricted comodule, with the same underlying submodule.

Equations

• TauCeti.Subcomodule.ofCorestrictOfSplit f r hr W = TauCeti.Subcomodule.ofSubmodule W.carrier ⋯

@[simp]

theorem TauCeti.Subcomodule.ofCorestrictOfSplit_toSubmodule {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k D V) : (ofCorestrictOfSplit f r hr W).toSubmodule = W.toSubmodule

Recovery from a split corestriction preserves the underlying submodule.

@[simp]

theorem TauCeti.Subcomodule.mem_ofCorestrictOfSplit {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k D V) (m : V) : m ∈ ofCorestrictOfSplit f r hr W ↔ m ∈ W

Membership is unchanged by recovery from a split corestriction.

@[simp]

theorem TauCeti.Subcomodule.corestrict_ofCorestrictOfSplit {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k D V) : corestrict f (ofCorestrictOfSplit f r hr W) = W

Corestricting a subcomodule recovered through a linear retraction gives the original.

@[simp]

theorem TauCeti.Subcomodule.ofCorestrictOfSplit_corestrict {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k C V) : ofCorestrictOfSplit f r hr (corestrict f W) = W

Recovering a corestricted subcomodule through a linear retraction gives the original.

def TauCeti.Subcomodule.corestrictOrderIsoOfSplit {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) : Subcomodule k C V ≃o Subcomodule k D V

The order isomorphism induced by a coalgebra morphism with a linear retraction preserves underlying submodules.

Equations

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

@[simp]

theorem TauCeti.Subcomodule.corestrictOrderIsoOfSplit_apply {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k C V) : (corestrictOrderIsoOfSplit f r hr) W = corestrict f W

The forward map of the split-corestriction order isomorphism is corestriction.

@[simp]

theorem TauCeti.Subcomodule.corestrictOrderIsoOfSplit_symm_apply {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) (W : Subcomodule k D V) : (corestrictOrderIsoOfSplit f r hr).symm W = ofCorestrictOfSplit f r hr W

The inverse map of the split-corestriction order isomorphism recovers the subcomodule.