feat(Analysis/InnerProductSpace/Quotient): add the quotient InnerProductSpace by the null space

[yoh-tanimoto]

Define the null space in the an InnerProductSpace without definite and add InnerProduceSpace structure to the quotient by the null space.

Motivation: in many application such as the GNS construction, one first constructs an InnerProductSpace then quotients it by the null space. This file realizes this latter passage.

Probably many basic lemmas are missing. Please tell me in comments.

---

• Depends on: [Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup #17007
• Depends on: [Merged by Bors] - chore(Analysis/InnerProductSpace/Dual): weaken assumptions to SeminormedAddCommGroup #17416
• Depends on: [Merged by Bors] - feat: add Normed instances for SeparationQuotient #17452

[github-actions]

PR summary e85a7857b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Group.SeparationQuotient	1265
Mathlib.Analysis.InnerProductSpace.SeparationQuotient	1627

---

Declarations diff

+ CLM_lift_apply
+ CommMonoidHom_lift_apply
+ IsQuotient
+ IsQuotient.norm_le
+ IsQuotient.norm_lift
+ Submodule.SeparationQuotient.normedSpace
+ bddBelow_image_norm
+ image_norm_nonempty
+ inn_nullSubmodule_right_eq_zero
+ innerQ
+ inner_eq_zero_of_left_mem_nullSubmodule
+ inner_nullSubmodule_right_eq_zero
+ inseparable_iff_norm_zero
+ instBoundedSMul
+ instModule
+ instance : InnerProductSpace 𝕜 (SeparationQuotient E)
+ instance : IsClosed ((nullSubmodule 𝕜 E) : Set E) := by
+ instance : Nonempty (@nullSubgroup M _) := ⟨0⟩
+ isClosed_nullSubgroup
+ isGLB_quotient_norm
+ isQuotientSeparationQuotient
+ ker_normedMk
+ lift
+ liftCLM_apply
+ liftMonoidHom
+ liftNormedAddGroupHom
+ liftNormedAddGroupHom_apply
+ lift_mk
+ lift_normNoninc
+ lift_norm_le
+ lift_unique
+ mem_nullSubmodule_iff
+ mkCLM
+ mkGroupHom
+ mk_eq_zero_iff
+ nhds_eq
+ normOnSeparationQuotient
+ norm_eq
+ norm_eq_infDist
+ norm_lift_apply_le
+ norm_lift_le
+ norm_lt_iff
+ norm_mk
+ norm_mk_eq
+ norm_mk_eq_sInf
+ norm_mk_eq_zero
+ norm_mk_le
+ norm_mk_nonneg
+ norm_mk_zero
+ norm_normedMk
+ norm_normedMk_le
+ norm_trivial_separaationQuotient_mk
+ normedAddCommGroupQuotient
+ normedCommRing
+ normedMk
+ normedMk.apply
+ nullSubgroup
+ nullSubmodule
+ nullSubmodule_le_ker_preInnerQ
+ nullSubmodule_le_ker_toDualMap
+ nullSubmodule_le_ker_toDualMap'
+ preInnerQ
+ quotient_nhd_basis
+ quotient_norm_add_le
+ quotient_norm_eq_zero_iff
+ quotient_norm_mk_eq
+ quotient_norm_neg
+ quotient_norm_nonneg
+ quotient_norm_sub_rev
+ surjective_normedMk
++ eq_of_inseparable
++ liftCLM

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[j-loreaux]

I suspect that this is not the way to proceed here. Instead, I recommend using SeparationQuotient.

If we don't already have it, you could show that if X is a Seminormed* then SeparationQuotient X is a Normed*. Then you could define the inner product space isntance on SeparationQuotient X.

The problem with putting this InnerProductSpace instance on E / nullSpace \bbk E is that we could end up with non-defeq instances later down the line. Moreover, SeparationQuotient does almost exactly what you want already, it just doesn't have the necessary instances yet.

[eric-wieser]

This isn't true, cauchy-schwarz is not used in this definition at all!

Note you can define this more generally as

variable {𝕜 E} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]

/-- The null space with respect to the norm. -/
def nullSpace : Submodule 𝕜 E where
  carrier := {x : E | ‖x‖ = 0}
  add_mem' {x y} (hx : ‖x‖ = 0) (hy : ‖y‖ = 0) := by
    apply le_antisymm _ (norm_nonneg _)
    refine (norm_add_le x y).trans_eq ?_
    rw [hx, hy, add_zero]
  zero_mem' := norm_zero
  smul_mem' c x (hx : ‖x‖ = 0) := by
    apply le_antisymm _ (norm_nonneg _)
    refine (norm_smul_le _ _).trans_eq ?_
    rw [hx, mul_zero]

[yoh-tanimoto]

I see, I will move the docstring to the beginning.

I get "failed to synthesize BoundedSMul 𝕜 E", although it is there... why?

import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.Normed.Group.Quotient

variable (𝕜 E : Type*) [k: RCLike 𝕜]

variable {𝕜 E} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]

/-- The null space with respect to the norm. -/
def nullSpace : Submodule 𝕜 E where
  carrier := {x : E | ‖x‖ = 0}
  add_mem' {x y} (hx : ‖x‖ = 0) (hy : ‖y‖ = 0) := by
    apply le_antisymm _ (norm_nonneg _)
    refine (norm_add_le x y).trans_eq ?_
    rw [hx, hy, add_zero]
  zero_mem' := norm_zero
  smul_mem' c x (hx : ‖x‖ = 0) := by
    apply le_antisymm _ (norm_nonneg _)
    refine (norm_smul_le _ _).trans_eq ?_
    rw [hx, mul_zero]

[eric-wieser]

You should remove [k: RCLike 𝕜], it conflicts with [SeminormedRing 𝕜]

[yoh-tanimoto]

Ah ok, thank you!

I think I will have to wait until I will have decided to use SeparationQuotient or the null space by hand.

[yoh-tanimoto]

@j-loreaux If I use SeparationQuotient and take the instance SeparationQuotient.instAddCommGroup, it is different from AddSubgroup.seminormedAddCommGroupQuotient, correct? Do I have to define the norm again for SeparationQuotient?

[j-loreaux]

Yes, it is certainly different, and you'll need to define the norm again, assuming the instance doesn't already exist. But I think this is the cleaner approach.

[eric-wieser]

I removed .carrier as suggested. In some places I had to use have : x ∈ nullSpace ↔ x ∈ (@nullSpace M _ : Set M) := by rfl. I wonder if there is a better way

This theorem is called SetLike.mem_coe

[yoh-tanimoto]

thank you, I replaced all the immediate have with SetLike.mem_coe.

[eric-wieser]

I think cleaner as

Suggested change

	simp only
	obtain ⟨x', hx'⟩ := surjective_mk x
	obtain ⟨y', hy'⟩ := surjective_mk y
	induction x with | _ x => ?_
	induction y with | _ y => ?_
	simp only

(untested)

[yoh-tanimoto]

It gave an error "tactic 'induction' failed, major premise type is not an inductive type Quot Setoid.r". I reverted it for the moment.

[yoh-tanimoto]

sorry, I wanted to change docstrings and theorem/instance names later. I know that the PR is still very much incomplete

[yoh-tanimoto]

I noticed that I need to define the lift of a linear map vanishing on the null space as a linear map. Where should I define it and how? In Mathlib.Topology.Algebra.SeparationQuotient as a CLM or Mathlib.Analysis.Normed.Group.SeparationQuotient?

[eric-wieser]

Here's a much shorter way to get the InnerProductSpace instance on SeparationQuotient:

import Mathlib.Analysis.InnerProductSpace.Basic

variable {𝕜 E} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]

namespace SeparationQuotient

instance : Inner 𝕜 (SeparationQuotient E) where
  inner := SeparationQuotient.lift₂ Inner.inner fun _ _ _ _ hab hcd =>
    ((hab.prod hcd).map continuous_inner).eq

theorem inner_mk_mk (x y : E) :
  inner (mk x) (mk y) = (inner x y : 𝕜) := rfl

instance : InnerProductSpace 𝕜 (SeparationQuotient E) where
  norm_sq_eq_inner := Quotient.ind norm_sq_eq_inner
  conj_symm := Quotient.ind₂ inner_conj_symm
  add_left := Quotient.ind fun x => Quotient.ind₂ <| inner_add_left x
  smul_left := Quotient.ind₂ inner_smul_left

end SeparationQuotient

[yoh-tanimoto]

ah! what should I do with this PR then?

[eric-wieser]

Probably the thing to do is go through the auxiliary lemmas you wrote and make PRs for the useful ones. Certainly we want the null space as a submodule, and the lift operations on separationQuotient look reasonable to have.