Documentation

LeanPool.MarkoffModP.BGS.Algebra.RatFuncLinearFractionalEquiv

Linear-fractional automorphisms of a rational function field #

An invertible matrix ((a, b), (c, d)) acts on K(X) by sending X to (aX+b)/(cX+d). This file constructs that action as a K-algebra equivalence and records its action on X and on embedded polynomials.

source
noncomputable def BGS.Algebra.ratFuncLinearFractionalValue {K : Type u_1} [Field K] (a b c d : K) :
RatFunc K

The value of the linear-fractional substitution associated to ((a, b), (c, d)) at the rational-function variable.

Equations
Instances For
    source
    theorem BGS.Algebra.ratFuncLinearFractional_denominator_ne_zero {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    RatFunc.C c * RatFunc.X + RatFunc.C d ≠ 0
    source
    theorem BGS.Algebra.ratFuncLinearFractionalValue_not_constant {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    ¬∃ (k : K), ratFuncLinearFractionalValue a b c d = RatFunc.C k
    source
    theorem BGS.Algebra.ratFuncLinearFractionalValue_transcendental {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    Transcendental K (ratFuncLinearFractionalValue a b c d)
    source
    theorem BGS.Algebra.ratFuncLinearFractionalValue_inverse_formula {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    RatFunc.X = (RatFunc.C d * ratFuncLinearFractionalValue a b c d - RatFunc.C b) / (RatFunc.C a - RatFunc.C c * ratFuncLinearFractionalValue a b c d)
    source
    theorem BGS.Algebra.adjoin_ratFuncLinearFractionalValue_eq_top {K : Type u_1} [Field K] {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    K⟮ratFuncLinearFractionalValue a b c d⟯ = ⊤
    source
    noncomputable def BGS.Algebra.ratFuncLinearFractionalEquiv {K : Type u_1} [Field K] (a b c d : K) (hdet : a * d - b * c ≠ 0) :
    Gal(RatFunc K/K)

    The K-algebra automorphism of K(X) induced by the invertible matrix ((a, b), (c, d)).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem BGS.Algebra.ratFuncLinearFractionalEquiv_apply_X {K : Type u_1} [Field K] (a b c d : K) (hdet : a * d - b * c ≠ 0) :
      (ratFuncLinearFractionalEquiv a b c d hdet) RatFunc.X = ratFuncLinearFractionalValue a b c d
      source
      @[simp]
      theorem BGS.Algebra.ratFuncLinearFractionalEquiv_apply_algebraMap {K : Type u_1} [Field K] (a b c d : K) (hdet : a * d - b * c ≠ 0) (f : Polynomial K) :
      (ratFuncLinearFractionalEquiv a b c d hdet) ((algebraMap (Polynomial K) (RatFunc K)) f) = (Polynomial.aeval (ratFuncLinearFractionalValue a b c d)) f