Documentation

instance instModuleMatrixFinOfNatNatProd {R : Type u_1} [Semiring R] :

Module (Matrix (Fin 2) (Fin 2) R) (R × R)

Equations

instance instSMulCommClassMatrixFinOfNatNatProd {R : Type u_1} [Semiring R] {S : Type u_3} [DistribSMul S R] [SMulCommClass R S R] :

SMulCommClass (Matrix (Fin 2) (Fin 2) R) S (R × R)

@[simp]

theorem Matrix.fin_two_smul_prod {R : Type u_1} [Semiring R] (g : Matrix (Fin 2) (Fin 2) R) (v : R × R) :

g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)

@[simp]

theorem Matrix.GeneralLinearGroup.fin_two_smul_prod {R : Type u_3} [CommRing R] (g : GL (Fin 2) R) (v : R × R) :

g • v = (↑g 0 0 * v.1 + ↑g 0 1 * v.2, ↑g 1 0 * v.1 + ↑g 1 1 * v.2)

def OnePoint.equivProjectivization (K : Type u_1) [DivisionRing K] [DecidableEq K] :

OnePoint K ≃ Projectivization K (K × K)

The one-point compactification of a division ring K is equivalent to the projectivization ℙ K (K × K).

Equations

Instances For

@[simp]

theorem OnePoint.equivProjectivization_apply_infinity (K : Type u_1) [DivisionRing K] [DecidableEq K] :

(equivProjectivization K) infty = Projectivization.mk K (1, 0) ⋯

@[simp]

theorem OnePoint.equivProjectivization_apply_coe (K : Type u_1) [DivisionRing K] [DecidableEq K] (t : K) :

(equivProjectivization K) ↑t = Projectivization.mk K (t, 1) ⋯

@[simp]

theorem OnePoint.equivProjectivization_symm_apply_mk (K : Type u_1) [DivisionRing K] [DecidableEq K] (x y : K) (h : (x, y) ≠ 0) :

(equivProjectivization K).symm (Projectivization.mk K (x, y) h) = if y = 0 then infty else ↑(y⁻¹ * x)

instance OnePoint.instGLAction {K : Type u_1} [Field K] [DecidableEq K] :

MulAction (GL (Fin 2) K) (OnePoint K)

For a field K, the group GL(2, K) acts on OnePoint K, via the canonical identification with the ℙ¹(K) (which is given explicitly by Möbius transformations).

Equations

theorem OnePoint.smul_infty_def {K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} :

g • infty = (equivProjectivization K).symm (Projectivization.mk K (↑g 0 0, ↑g 1 0) ⋯)

theorem OnePoint.smul_infty_eq_ite {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) :

g • infty = if ↑g 1 0 = 0 then infty else ↑(↑g 0 0 / ↑g 1 0)

theorem OnePoint.smul_infty_eq_self_iff {K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} :

g • infty = infty ↔ ↑g 1 0 = 0

theorem OnePoint.smul_some_eq_ite {K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} {k : K} :

g • ↑k = if ↑g 1 0 * k + ↑g 1 1 = 0 then infty else ↑((↑g 0 0 * k + ↑g 0 1) / (↑g 1 0 * k + ↑g 1 1))

theorem OnePoint.map_smul {K : Type u_1} [Field K] [DecidableEq K] {L : Type u_2} [Field L] [DecidableEq L] (f : K →+* L) (g : GL (Fin 2) K) (c : OnePoint K) :

OnePoint.map (⇑f) (g • c) = (Matrix.GeneralLinearGroup.map f) g • OnePoint.map (⇑f) c

theorem Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff {K : Type u_1} [Field K] [DecidableEq K] {c : K} {g : GL (Fin 2) K} :

(Polynomial.aeval c) g.fixpointPolynomial = 0 ↔ g • ↑c = ↑c

The roots of g.fixpointPolynomial are the fixed points of g ∈ GL(2, K) acting on the finite part of OnePoint K.

def Matrix.GeneralLinearGroup.parabolicFixedPoint {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) :

OnePoint K

If g is parabolic, this is the unique fixed point of g in OnePoint K.

Equations

Instances For

theorem Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff {K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} (hg : g.IsParabolic) [NeZero 2] {c : OnePoint K} :

g • c = c ↔ c = g.parabolicFixedPoint

theorem Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow {K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} (hg : g.IsParabolic) [CharZero K] {n : ℕ} (hn : n ≠ 0) :

(g ^ n).parabolicFixedPoint = g.parabolicFixedPoint