instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic

English

Instance: HasDetPlusMinusOne Γ from HasDetOne Γ.

Русский

Экземпляр: HasDetPlusMinusOne Γ получаем из HasDetOne Γ.

LaTeX

$$instance HasDetPlusMinusOne Γ := ⟨fun {g} hg => by simp [HasDetOne.det_eq hg]⟩$$

Lean4

instance {Γ : Subgroup (GL (Fin 2) ℝ)} [h : Γ.IsArithmetic] : HasDetPlusMinusOne Γ :=
  by
  refine ⟨fun {g} hg ↦ ?_⟩
  suffices |g.det.val| = 1 by rcases abs_cases g.det.val <;> aesop
  obtain ⟨n, hn, _, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero Subgroup.IsArithmetic.is_commensurable.2 hg
  suffices |(g.det ^ n).val| = 1 by simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]
  obtain ⟨t, ht⟩ := hgn.1
  have := congr_arg Matrix.GeneralLinearGroup.det ht.symm
  rw [Matrix.SpecialLinearGroup.det_mapGL, map_pow] at this
  simp [this]

Похожие утверждения