ReflectionPlane.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Linear reflection products and common root planes for nondegenerate ambient forms.

theorem OAI.KLInvariance.ReflectionPlane.formPair_surjective line 16
Source documentation
Independent linear forms give a surjection to the coordinate plane.
```
theorem formPair_surjective (f g : Module.Dual k V)
    (hfg : LinearIndependent k ![f, g]) : Function.Surjective (f.prod g) := by
…
```

theorem OAI.KLInvariance.ReflectionPlane.range_preReflection_product_sub_id line 44

Source documentation

The range of the difference of a two-reflection product from the identity is exactly the span of the two roots.

theorem range_preReflection_product_sub_id (α β : V) (f g : Module.Dual k V)
    (hfg : LinearIndependent k ![f, g]) :
    LinearMap.range ((Module.preReflection α f).comp (Module.preReflection β g) -
      LinearMap.id) = Submodule.span k {α, β} := by
…

theorem OAI.KLInvariance.ReflectionPlane.range_reflection_product_sub_id line 68

theorem OAI.KLInvariance.ReflectionPlane.plane_eq_of_reflection_product_eq line 84

Source documentation

Equal products of two normalized reflections recover equal root planes, the exact local geometric input to dih:transport.

theorem plane_eq_of_reflection_product_eq
    (B : LinearMap.BilinForm k V) (hB : B.Nondegenerate)
    (α β γ δ : V)
    (hα : B α α = 2) (hβ : B β β = 2) (hγ : B γ γ = 2) (hδ : B δ δ = 2)
    (hαβ : LinearIndependent k ![α, β]) (hγδ : LinearIndependent k ![γ, δ])
    (heq : (Module.reflection hα).toLinearMap.comp (Module.reflection hβ).toLinearMap =
      (Module.reflection hγ).toLinearMap.comp (Module.reflection hδ).toLinearMap) :
    Submodule.span k {α, β} = Submodule.span k {γ, δ} := by
…