The kernel of an operator paired with a complementary coordinate

A continuous linear map A : M →L[R] F together with a second map q : M →L[R] G describes M by "the value of A" and "the remaining coordinate q" exactly when the pair A.prod q : M →L[R] F × G is invertible. That is the situation the implicit function theorem creates: there A is the derivative of the equation and q is a projection onto a complement of its kernel.

In that situation the second coordinate restricts to an isomorphism from ker A onto G. This file constructs its inverse, ContinuousLinearMap.kerSection, which sends v : G to the unique x : M with A x = 0 and q x = v, and packages it as ContinuousLinearMap.kerEquivOfProd : G ≃L[R] ↥A.ker. The kernel of A is therefore described by a continuous linear parametrization whose parameter space does not depend on the point at which A is taken, which is what lets a moving kernel — a tangent space along a level set — be compared with a fixed model space.

Invertibility of the pair is recorded through ContinuousLinearMap.IsInvertible, so that the section is a plain definition and the hypothesis appears only in the lemmas about it; the underlying inverse is Mathlib's total ContinuousLinearMap.inverse.

Main declarations

• ContinuousLinearMap.kerSection: the section G →L[R] M of q with values in ker A.
• ContinuousLinearMap.eq_kerSection: it is the only map with that defining property.
• ContinuousLinearMap.range_kerSection: its range is exactly ker A.
• ContinuousLinearMap.kerEquivOfProd: the resulting isomorphism G ≃L[R] ↥A.ker.

noncomputable def ContinuousLinearMap.kerSection {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] (A : M →L[R] F) (q : M →L[R] G) : G →L[R] M

The section of q with values in the kernel of A: it sends v : G to the unique x : M with A x = 0 and q x = v.

This is meaningful when the pair A.prod q is invertible, which every lemma below assumes; outside that case Mathlib's ContinuousLinearMap.inverse returns 0 and so does this map.

Equations

• A.kerSection q = (A.prod q).inverse ∘SL ContinuousLinearMap.inr R F G

theorem ContinuousLinearMap.prod_apply_kerSection {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (v : G) : (A.prod q) ((A.kerSection q) v) = (0, v)

The defining property of the section: the pair (A, q) sends A.kerSection q v to (0, v). Not a simp lemma: its two components, ContinuousLinearMap.apply_kerSection and ContinuousLinearMap.apply_kerSection_right, are, and together they prove it.

@[simp]

theorem ContinuousLinearMap.apply_kerSection {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (v : G) : A ((A.kerSection q) v) = 0

The section takes values in the kernel of A.

theorem ContinuousLinearMap.kerSection_mem_ker {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (v : G) : (A.kerSection q) v ∈ (↑A).ker

The Submodule.mem form of ContinuousLinearMap.apply_kerSection.

@[simp]

theorem ContinuousLinearMap.apply_kerSection_right {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (v : G) : q ((A.kerSection q) v) = v

The section is a right inverse of q.

@[simp]

theorem ContinuousLinearMap.kerSection_apply_of_mem_ker {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) {x : M} (hx : x ∈ (↑A).ker) : (A.kerSection q) (q x) = x

On the kernel of A the section undoes q.

theorem ContinuousLinearMap.eq_kerSection {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) {g : G →L[R] M} (hg : ∀ (v : G), (A.prod q) (g v) = (0, v)) : g = A.kerSection q

The section is characterised by its defining property. Any continuous linear map sent to (0, v) by the pair is ContinuousLinearMap.kerSection, so consumers never need to unfold the definition.

theorem ContinuousLinearMap.kerSection_injective {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) : Function.Injective ⇑(A.kerSection q)

The section is injective, being a right inverse of q.

@[simp]

theorem ContinuousLinearMap.range_kerSection {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) : (↑(A.kerSection q)).range = (↑A).ker

The kernel of A is exactly the range of the section.

noncomputable def ContinuousLinearMap.kerEquivOfProd {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] (A : M →L[R] F) (q : M →L[R] G) (h : (A.prod q).IsInvertible) : G ≃L[R] ↥(↑A).ker

An invertible pair identifies the kernel of its first component with the codomain of its second. The isomorphism is the restriction of q; its inverse is ContinuousLinearMap.kerSection.

Equations

• A.kerEquivOfProd q h = ContinuousLinearEquiv.equivOfInverse ((A.kerSection q).codRestrict (↑A).ker ⋯) (q ∘SL (↑A).ker.subtypeL) ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.coe_kerEquivOfProd_apply {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (v : G) : ↑((A.kerEquivOfProd q h) v) = (A.kerSection q) v

The isomorphism G ≃L[R] ↥A.ker is the section, read in the ambient space.

@[simp]

theorem ContinuousLinearMap.kerEquivOfProd_symm_apply {R : Type u_1} {M : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid F] [TopologicalSpace F] [Module R F] [AddCommMonoid G] [TopologicalSpace G] [Module R G] {A : M →L[R] F} {q : M →L[R] G} (h : (A.prod q).IsInvertible) (x : ↥(↑A).ker) : (A.kerEquivOfProd q h).symm x = q ↑x

Its inverse is the restriction of q to the kernel of A.