Extending a submodule basis by a quotient basis, indexed by Fin (m + n)

Module.Basis.sumQuot combines a basis of a submodule p of V with a basis of V ⧸ p into a basis of V indexed by a sum type. An induction on Module.finrank wants that basis indexed by Fin (m + n) instead, so that the two blocks are picked out by Fin.castAdd and Fin.natAdd and the resulting matrices are visibly block triangular.

This file records that reindexing together with the six equations locating the blocks: what the basis is on each block, what the coordinates of a vector are there, and the two _of_mem variants stated for an ambient vector known to lie in the submodule. It then computes the matrix, in this basis, of an endomorphism preserving the submodule: its diagonal blocks are the matrices of the restriction and of the induced endomorphism of the quotient, and its lower-left block vanishes. So the matrix is upper (uni)triangular as soon as both diagonal blocks are.

Main definitions

• TauCeti.extensionBasis: the Fin (m + n)-indexed basis of V built from a basis of p and a basis of V ⧸ p.

Main results

• TauCeti.extensionBasis_castAdd and TauCeti.extensionBasis_natAdd_mkQ: the basis vectors on the two blocks.
• TauCeti.extensionBasis_repr_castAdd and TauCeti.extensionBasis_repr_natAdd: the coordinates of a vector on the two blocks.
• TauCeti.extensionBasis_repr_castAdd_of_mem and TauCeti.extensionBasis_repr_natAdd_of_mem: the same for an ambient vector known to lie in the submodule, whose second-block coordinates vanish.
• TauCeti.toMatrixAlgEquiv_extensionBasis_castAdd_castAdd, TauCeti.toMatrixAlgEquiv_extensionBasis_natAdd_castAdd and TauCeti.toMatrixAlgEquiv_extensionBasis_natAdd_natAdd: the blocks of the matrix of an endomorphism preserving the submodule.
• TauCeti.toMatrixAlgEquiv_extensionBasis_isUpperTriangular and TauCeti.toMatrixAlgEquiv_extensionBasis_isUpperUnitriangular: that matrix is upper (uni)triangular when both of its diagonal blocks are.

noncomputable def TauCeti.extensionBasis {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) : Module.Basis (Fin (m + n)) R V

Extend bases of a submodule and of its quotient to a basis of the ambient module, indexed by Fin (m + n).

Equations

• TauCeti.extensionBasis p bp bq = (bp.sumQuot bq).reindex finSumFinEquiv

@[simp]

theorem TauCeti.extensionBasis_castAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (i : Fin m) : (extensionBasis p bp bq) (Fin.castAdd n i) = ↑(bp i)

On the first block, extensionBasis is the given basis of the submodule.

@[simp]

theorem TauCeti.extensionBasis_natAdd_mkQ {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (j : Fin n) : Submodule.Quotient.mk ((extensionBasis p bp bq) (Fin.natAdd m j)) = bq j

On the second block, extensionBasis lifts the given basis of the quotient.

theorem TauCeti.extensionBasis_repr_castAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (x : ↥p) (i : Fin m) : ((extensionBasis p bp bq).repr ↑x) (Fin.castAdd n i) = (bp.repr x) i

The first-block coordinates of a vector of the submodule are its coordinates there.

Not a simp lemma: extensionBasis_repr_castAdd_of_mem is the simp normal form, matching how Mathlib annotates Module.Basis.sumQuot_repr_inl and sumQuot_repr_inl_of_mem.

@[simp]

theorem TauCeti.extensionBasis_repr_natAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (x : V) (j : Fin n) : ((extensionBasis p bp bq).repr x) (Fin.natAdd m j) = (bq.repr (p.mkQ x)) j

The second-block coordinates of a vector are the coordinates of its quotient class.

@[simp]

theorem TauCeti.extensionBasis_repr_castAdd_of_mem {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (x : V) (hx : x ∈ p) (i : Fin m) : ((extensionBasis p bp bq).repr x) (Fin.castAdd n i) = (bp.repr ⟨x, hx⟩) i

The first-block coordinates of an ambient vector lying in the submodule are its coordinates there.

theorem TauCeti.extensionBasis_repr_natAdd_of_mem {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) (x : V) (hx : x ∈ p) (j : Fin n) : ((extensionBasis p bp bq).repr x) (Fin.natAdd m j) = 0

A vector of the submodule has no second-block coordinates: this is the vanishing of the off-diagonal block.

Not a simp lemma: extensionBasis_repr_natAdd above already is, so this left-hand side is not in simp normal form and marking it trips simpNF. Mathlib annotates its sumQuot counterparts the same way — sumQuot_repr_inr is simp and sumQuot_repr_inr_of_mem is not.

@[simp]

theorem TauCeti.toMatrixAlgEquiv_extensionBasis_castAdd_castAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) {f : Module.End R V} (hf : p ≤ Submodule.comap f p) (i j : Fin m) : (LinearMap.toMatrixAlgEquiv (extensionBasis p bp bq)) f (Fin.castAdd n i) (Fin.castAdd n j) = (LinearMap.toMatrixAlgEquiv bp) (LinearMap.restrict f ⋯) i j

In the basis extensionBasis p bp bq, the diagonal block of an endomorphism f preserving p indexed by the basis bp of p is the matrix of the restriction of f to p.

@[simp]

theorem TauCeti.toMatrixAlgEquiv_extensionBasis_natAdd_castAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) {f : Module.End R V} (hf : p ≤ Submodule.comap f p) (i : Fin n) (j : Fin m) : (LinearMap.toMatrixAlgEquiv (extensionBasis p bp bq)) f (Fin.natAdd m i) (Fin.castAdd n j) = 0

In the basis extensionBasis p bp bq, the lower-left block of the matrix of an endomorphism preserving p vanishes.

@[simp]

theorem TauCeti.toMatrixAlgEquiv_extensionBasis_natAdd_natAdd {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) {f : Module.End R V} (hf : p ≤ Submodule.comap f p) (i j : Fin n) : (LinearMap.toMatrixAlgEquiv (extensionBasis p bp bq)) f (Fin.natAdd m i) (Fin.natAdd m j) = (LinearMap.toMatrixAlgEquiv bq) (p.mapQ p f hf) i j

In the basis extensionBasis p bp bq, the diagonal block of an endomorphism f preserving p indexed by the basis bq of V ⧸ p is the matrix of the endomorphism of V ⧸ p induced by f.

theorem TauCeti.toMatrixAlgEquiv_extensionBasis_isUpperTriangular {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) {f : Module.End R V} (hf : p ≤ Submodule.comap f p) (hp : ((LinearMap.toMatrixAlgEquiv bp) (LinearMap.restrict f ⋯)).IsUpperTriangular) (hq : ((LinearMap.toMatrixAlgEquiv bq) (p.mapQ p f hf)).IsUpperTriangular) : ((LinearMap.toMatrixAlgEquiv (extensionBasis p bp bq)) f).IsUpperTriangular

If an endomorphism f preserves a submodule p and its restriction to p and the induced endomorphism of V ⧸ p have upper-triangular matrices in the bases bp and bq, then the matrix of f in the extension basis extensionBasis p bp bq is upper triangular.

theorem TauCeti.toMatrixAlgEquiv_extensionBasis_isUpperUnitriangular {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {m n : ℕ} (p : Submodule R V) (bp : Module.Basis (Fin m) R ↥p) (bq : Module.Basis (Fin n) R (V ⧸ p)) {f : Module.End R V} (hf : p ≤ Submodule.comap f p) (hp : ((LinearMap.toMatrixAlgEquiv bp) (LinearMap.restrict f ⋯)).IsUpperUnitriangular) (hq : ((LinearMap.toMatrixAlgEquiv bq) (p.mapQ p f hf)).IsUpperUnitriangular) : ((LinearMap.toMatrixAlgEquiv (extensionBasis p bp bq)) f).IsUpperUnitriangular

If an endomorphism f preserves a submodule p and its restriction to p and the induced endomorphism of V ⧸ p have upper-unitriangular matrices in the bases bp and bq, then the matrix of f in the extension basis extensionBasis p bp bq is upper unitriangular.

noncomputable def LinearMap.rangeExtensionBasis {k : Type u_1} {V : Type u_2} {W : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {m n : ℕ} (f : V →ₗ[k] W) (I : Submodule k V) (hker : f.ker ≤ I) (bImage : Module.Basis (Fin m) k ↥(Submodule.map f.rangeRestrict I)) (bQuot : Module.Basis (Fin n) k (V ⧸ I)) : Module.Basis (Fin (m + n)) k ↥f.range

Extend bases of the image of a submodule and of its quotient to a basis of a map's range.

Equations

• f.rangeExtensionBasis I hker bImage bQuot = TauCeti.extensionBasis (Submodule.map f.rangeRestrict I) bImage (bQuot.map (f.quotientEquivRangeQuotientMap I hker))

theorem LinearMap.rangeExtensionBasis_natAdd_mkQ {k : Type u_1} {V : Type u_2} {W : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {m n : ℕ} (f : V →ₗ[k] W) (I : Submodule k V) (hker : f.ker ≤ I) (bImage : Module.Basis (Fin m) k ↥(Submodule.map f.rangeRestrict I)) (bQuot : Module.Basis (Fin n) k (V ⧸ I)) (j : Fin n) : Submodule.Quotient.mk ((f.rangeExtensionBasis I hker bImage bQuot) (Fin.natAdd m j)) = (f.quotientEquivRangeQuotientMap I hker) (bQuot j)

The quotient block of the range extension basis is the transported quotient basis.

theorem LinearMap.rangeExtensionBasis_castAdd {k : Type u_1} {V : Type u_2} {W : Type u_3} [CommRing k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {m n : ℕ} (f : V →ₗ[k] W) (I : Submodule k V) (hker : f.ker ≤ I) (bImage : Module.Basis (Fin m) k ↥(Submodule.map f.rangeRestrict I)) (bQuot : Module.Basis (Fin n) k (V ⧸ I)) (i : Fin m) : (f.rangeExtensionBasis I hker bImage bQuot) (Fin.castAdd n i) = ↑(bImage i)

The image block of the range extension basis is the given image basis.