theorem Oriflamme.extend_lagrangian_auto_det {k : Type u_1} [Field k] {U : Type u_2} {U' : Type u_3} {V : Type u_4} [AddCommGroup U] [AddCommGroup U'] [AddCommGroup V] [Module k U] [Module k U'] [Module k V] [Module.Free k U] [Module.Free k U'] [Module.Finite k U] [Module.Finite k U'] (e : (U × U') ≃ₗ[k] V) (α : U ≃ₗ[k] U) (β : U' ≃ₗ[k] U') : have h := ↑e ∘ₗ (↑α).prodMap ↑β ∘ₗ ↑e.symm; LinearMap.det h = LinearMap.det ↑α * LinearMap.det ↑β

Given an isomorphism $e : U \oplus U' \cong V$ and automorphisms $\alpha$ of $U$, $\beta$ of $U'$, the conjugated map $h = e \circ (\alpha \oplus \beta) \circ e^{-1}$ has determinant $\det h = \det \alpha \cdot \det \beta$.

theorem Oriflamme.extend_lagrangian_auto_det_one {k : Type u_1} [Field k] {U : Type u_2} {U' : Type u_3} {V : Type u_4} [AddCommGroup U] [AddCommGroup U'] [AddCommGroup V] [Module k U] [Module k U'] [Module k V] [Module.Free k U] [Module.Free k U'] [Module.Finite k U] [Module.Finite k U'] (e : (U × U') ≃ₗ[k] V) (α : U ≃ₗ[k] U) (β : U' ≃ₗ[k] U') (hβ : LinearMap.det ↑β = (LinearMap.det ↑α)⁻¹) : have h := ↑e ∘ₗ (↑α).prodMap ↑β ∘ₗ ↑e.symm; LinearMap.det h = 1

Specialization: if $\det \beta = (\det \alpha)^{-1}$, then the extended automorphism $h$ has determinant $1$, lying in the special isometry group.

theorem Oriflamme.extend_lagrangian_auto_restricts {k : Type u_1} [Field k] {U : Type u_2} {U' : Type u_3} {V : Type u_4} [AddCommGroup U] [AddCommGroup U'] [AddCommGroup V] [Module k U] [Module k U'] [Module k V] (e : (U × U') ≃ₗ[k] V) (α : U ≃ₗ[k] U) (β : U' ≃ₗ[k] U') : have h := ↑e ∘ₗ (↑α).prodMap ↑β ∘ₗ ↑e.symm; ∀ (u : U), h (e (u, 0)) = e (α u, 0)

The extended automorphism $h$ restricted to the Lagrangian subspace $e(U \times \{0\})$ acts as $\alpha$: $h(e(u, 0)) = e(\alpha u, 0)$.

theorem Oriflamme.extend_lagrangian_auto_isometry {k : Type u_1} [Field k] {U : Type u_2} {U' : Type u_3} {V : Type u_4} [AddCommGroup U] [AddCommGroup U'] [AddCommGroup V] [Module k U] [Module k U'] [Module k V] (e : (U × U') ≃ₗ[k] V) (α : U ≃ₗ[k] U) (β : U' ≃ₗ[k] U') (B : V →ₗ[k] V →ₗ[k] k) (hU_iso : ∀ (u₁ u₂ : U), (B (e (u₁, 0))) (e (u₂, 0)) = 0) (hU'_iso : ∀ (u'₁ u'₂ : U'), (B (e (0, u'₁))) (e (0, u'₂)) = 0) (hadj : ∀ (u : U) (u' : U'), (B (e (α u, 0))) (e (0, β u')) = (B (e (u, 0))) (e (0, u'))) (hadj' : ∀ (u' : U') (u : U), (B (e (0, β u'))) (e (α u, 0)) = (B (e (0, u'))) (e (u, 0))) : have h := ↑e ∘ₗ (↑α).prodMap ↑β ∘ₗ ↑e.symm; ∀ (v w : V), (B (h v)) (h w) = (B v) w

Lagrangian extension is an isometry: given that $e(U \times \{0\})$ and $e(\{0\} \times U')$ are isotropic Lagrangians and $\alpha, \beta$ are mutually adjoint, the extended map $h = e \circ (\alpha \oplus \beta) \circ e^{-1}$ preserves the bilinear form $B$.