[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : f ∈ skewAdjointSubmodule B
hg : g ∈ skewAdjointSubmodule B
⊢ ⁅f, g⁆ ∈ skewAdjointSubmodule B
[PROOFSTEP]
rw [mem_skewAdjointSubmodule] at *
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hf.mul hg
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsAdjointPair B B (f * g) (g * f)
[PROOFSTEP]
rw [← neg_mul_neg g f]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
⊢ IsAdjointPair B B (f * g) (-g * -f)
[PROOFSTEP]
exact hf.mul hg
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hg.mul hf
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsAdjointPair B B (g * f) (f * g)
[PROOFSTEP]
rw [← neg_mul_neg f g]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
⊢ IsAdjointPair B B (g * f) (-f * -g)
[PROOFSTEP]
exact hg.mul hf
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsSkewAdjoint B ⁅f, g⁆
[PROOFSTEP]
change BilinForm.IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
[PROOFSTEP]
rw [neg_sub]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint B f
hg : IsSkewAdjoint B g
hfg : IsAdjointPair B B (f * g) (g * f)
hgf : IsAdjointPair B B (g * f) (f * g)
⊢ IsAdjointPair B B (f * g - g * f) (g * f - f * g)
[PROOFSTEP]
exact hfg.sub hgf
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ { x // x ∈ skewAdjointLieSubalgebra (comp B ↑e ↑e) } ≃ₗ⁅R⁆ { x // x ∈ skewAdjointLieSubalgebra B }
[PROOFSTEP]
apply LieEquiv.ofSubalgebras _ _ e.lieConj
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
⊢ LieSubalgebra.map (LinearEquiv.lieConj e).toLieHom (skewAdjointLieSubalgebra (comp B ↑e ↑e)) =
    skewAdjointLieSubalgebra B
[PROOFSTEP]
ext f
[GOAL]
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ f ∈ LieSubalgebra.map (LinearEquiv.lieConj e).toLieHom (skewAdjointLieSubalgebra (comp B ↑e ↑e)) ↔
    f ∈ skewAdjointLieSubalgebra B
[PROOFSTEP]
simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
[GOAL]
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ ↑(LinearEquiv.symm (LieEquiv.toLinearEquiv (LinearEquiv.lieConj e))) f ∈
      (skewAdjointLieSubalgebra (comp B ↑e ↑e)).toSubmodule ↔
    f ∈ skewAdjointLieSubalgebra B
[PROOFSTEP]
exact (BilinForm.isPairSelfAdjoint_equiv (-B) B e f).symm
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : { x // x ∈ skewAdjointLieSubalgebra (comp B ↑e ↑e) }
⊢ ↑(↑(skewAdjointLieSubalgebraEquiv B e) f) = ↑(LinearEquiv.lieConj e) ↑f
[PROOFSTEP]
simp [skewAdjointLieSubalgebraEquiv]
[GOAL]
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : { x // x ∈ skewAdjointLieSubalgebra B }
⊢ ↑(↑(LieEquiv.symm (skewAdjointLieSubalgebraEquiv B e)) f) = ↑(LinearEquiv.lieConj (LinearEquiv.symm e)) ↑f
[PROOFSTEP]
simp [skewAdjointLieSubalgebraEquiv]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
⊢ (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ
[PROOFSTEP]
simp
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : A ∈ skewAdjointMatricesSubmodule J
hB : B ∈ skewAdjointMatricesSubmodule J
⊢ ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
[PROOFSTEP]
simp only [mem_skewAdjointMatricesSubmodule] at *
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ IsSkewAdjoint J ⁅A, B⁆
[PROOFSTEP]
change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : IsSkewAdjoint J A
hB : IsSkewAdjoint J B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
change Aᵀ * J = J * (-A) at hA 
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : IsSkewAdjoint J B
hA : Aᵀ * J = J * -A
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
change Bᵀ * J = J * (-B) at hB 
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
[PROOFSTEP]
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket, sub_mul, mul_assoc,
  mul_assoc, hA, hB, ← mul_assoc, ← mul_assoc, hA, hB]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)
[PROOFSTEP]
noncomm_ring
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
⊢ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
ext A
[GOAL]
case h
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ A ∈ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
  by
  simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
  exact this
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ A ∈ LieSubalgebra.map (LieEquiv.symm (Matrix.lieConj P h)).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
simp only [LieSubalgebra.mem_coe, Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule, LinearEquiv.coe_coe]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ ↑(LinearEquiv.symm (LieEquiv.toLinearEquiv (LieEquiv.symm (Matrix.lieConj P h)))) A ∈
      (skewAdjointMatricesLieSubalgebra J).toSubmodule ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
[PROOFSTEP]
exact this
[GOAL]
case h
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ ↑(Matrix.lieConj P h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
[PROOFSTEP]
simp [Matrix.IsSkewAdjoint, J.isAdjointPair_equiv' _ _ P (isUnit_of_invertible P)]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J P : Matrix n n R
h : Invertible P
A : { x // x ∈ skewAdjointMatricesLieSubalgebra J }
⊢ ↑(↑(skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P
[PROOFSTEP]
simp [skewAdjointMatricesLieSubalgebraEquiv]
[GOAL]
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
⊢ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
ext A
[GOAL]
case h
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
⊢ A ∈ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
  -- Porting note: Originally `simpa [this]`simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
[GOAL]
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
this : Matrix.IsSkewAdjoint J (↑(AlgEquiv.symm e) A) ↔ Matrix.IsSkewAdjoint (↑e J) A
⊢ A ∈ LieSubalgebra.map (AlgEquiv.toLieEquiv e).toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (↑e J)
[PROOFSTEP]
simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
[GOAL]
case h
R : Type u
n : Type w
inst✝⁴ : CommRing R
inst✝³ : DecidableEq n
inst✝² : Fintype n
J : Matrix n n R
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h : ∀ (A : Matrix n n R), (↑e A)ᵀ = ↑e Aᵀ
A : Matrix m m R
⊢ Matrix.IsSkewAdjoint J (↑(AlgEquiv.symm e) A) ↔ Matrix.IsSkewAdjoint (↑e J) A
[PROOFSTEP]
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h, ← Function.Injective.eq_iff e.injective, map_mul,
  AlgEquiv.apply_symm_apply, map_neg]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J
[PROOFSTEP]
change A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
[PROOFSTEP]
simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]
[GOAL]
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
⊢ Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A
[PROOFSTEP]
simpa using congr_arg (fun B => u⁻¹ • B) h
[GOAL]
case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J✝ : Matrix n n R
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A
[PROOFSTEP]
simp [h]
