Orthogonality for affine subspaces

[urkud]

• Define AffineSubspace.IsOrtho s t as s.direction ⟂ t.direction and develop basic API (mostly copy from
  Submodule.IsOrtho). Additions specific to affine subspaces
  include lemmas like IsOrtho.trans_parallel.

• Define AffineSubspace.orthogonal, e.g., as

  /-- Orthogonal complement to an affine subspace passing through a given point. -/
  def orthogonal (s : AffineSubspace ℝ P) (b : P) : AffineSubspace ℝ P :=
  .comap (AffineMap.id ℝ P -ᵥ AffineMap.const ℝ P b) (s.directionᗮ).toAffineSubspace

  and prove lemmas like "orthogonal complements through different
  points are parallel", "orthogonal complements to parallel affine
  subspaces are parallel" (+ an iff version assuming that the
  subspaces are closed).

[jsm28]

The existing idiom for "Orthogonal complement to an affine subspace passing through a given point." is AffineSubspace.mk' b s.directionᗮ, which is used in various places (sometimes with the AffineSubspace namespace open so it's just mk' b s.directionᗮ) and also seems simpler than the definition used here.

[urkud]

Thank you! Indeed, the current idiom is shorter but I think that we should have a def and API for that.

BTW, should we change mk' to use "vsub belongs to the direction" instead of the current "exists"? Then our definitions will be defeq.

[MithicSpirit]

Hey, I'm working on this issue but just wondering what file this should be put in. I've been thinking that it should either go in the same file as Submodule.orthogonal, in a new file (AffineSubspace.lean) in that same folder, or in a new file at LinearAlgebra/AffineSpace/Orthogonal.lean.

Also quick note that I think that the iff lemma asked for above also requires that the subspaces be nonempty, as the case when one subspace is empty and the other is a singleton causes issues.

[urkud]

It should go to a new file. The name is not that important but it should be somewhere in Analysis.InnerProductSpace.*.
About iff: it's quite possible that I missed some degenerate case. One of good things about Lean is that it'll force you to fix this.

[jsm28]

I'm not particularly concerned with exactly what mk' is defeq to; anything that cares about that defeq is either part of setting up the API for mk' or should be changed to use that API.