Documentation

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Projective general linear group #

In this file we define Matrix.ProjGenLinGroup n R as the quotient of GL n R by its center. We introduce notation PGL(n, R) for this group, which works if n is either a finite type or a natural number. If n is a number, then PGL(n, R) is interpreted as PGL(Fin n, R).

source
🔸 coverage
def Matrix.ProjGenLinGroup (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
Type (max (max u_1 u_2) u_2 u_1)

Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance Matrix.instGroupProjGenLinGroup (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
    Group (ProjGenLinGroup n R)
    source
    🔸 coverage
    def MatrixGroups.«termPGL(_,_)» :
    Lean.ParserDescr

    Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

    Instances For
      source
      🔸 coverage
      def MatrixGroups.«termPGL(_,_)_1» :
      Lean.ParserDescr

      Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

      Instances For
        source
        🔸 coverage
        def Matrix.ProjGenLinGroup.mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :
        GL n R →* ProjGenLinGroup n R

        The natural projection from GL n R to PGL n R.

        Instances For
          source
          📐 coverage
          theorem Matrix.ProjGenLinGroup.mk_surjective {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :
          Function.Surjective ⇑mk
          source
          📐 coverage
          @[simp]
          theorem Matrix.ProjGenLinGroup.ker_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] :
          mk.ker = Subgroup.center (GL n R)
          source
          📐 coverage
          @[simp]
          theorem Matrix.ProjGenLinGroup.mk_scalar {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (u : Rˣ) :
          mk ((GeneralLinearGroup.scalar n) u) = 1
          source
          theorem Matrix.ProjGenLinGroup.induction_on {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {motive : ProjGenLinGroup n R → Prop} (g : ProjGenLinGroup n R) (mk : ∀ (g : GL n R), motive (mk g)) :
          motive g
          source
          🔸 coverage
          def Matrix.ProjGenLinGroup.lift {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] (f : GL n R →* M) (hf : f.comp (GeneralLinearGroup.scalar n) = 1) :
          ProjGenLinGroup n R →* M

          Lift a monoid homomorphism f : GL n R →* M that vanishes on all scalar matrices to a homomorphism from PGL(n, R).

          Instances For
            source
            📐 coverage
            @[simp]
            theorem Matrix.ProjGenLinGroup.lift_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] {f : GL n R →* M} (hf : f.comp (GeneralLinearGroup.scalar n) = 1) (g : GL n R) :
            (lift f hf) (mk g) = f g
            source
            📐 coverage
            @[simp]
            theorem Matrix.ProjGenLinGroup.lift_comp_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] {f : GL n R →* M} (hf : f.comp (GeneralLinearGroup.scalar n) = 1) :
            (lift f hf).comp mk = f
            source
            🔸 coverage
            @[implicit_reducible]
            def Matrix.ProjGenLinGroup.mulActionOfGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {α : Type u_4} [MulAction (GL n R) α] (h : ∀ (u : Rˣ) (a : α), (GeneralLinearGroup.scalar n) u • a = a) :
            MulAction (ProjGenLinGroup n R) α

            Given an action of GL n R such that the scalar matrices act trivially, define an action of PGL n R.

            Instances For
              source
              📐 coverage
              theorem Matrix.ProjGenLinGroup.mk_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {α : Type u_4} [MulAction (GL n R) α] (h : ∀ (u : Rˣ) (a : α), (GeneralLinearGroup.scalar n) u • a = a) (g : GL n R) (a : α) :
              mk g • a = g • a
              source
              🔸 coverage
              def Matrix.ProjGenLinGroup.signDet {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] :
              ProjGenLinGroup n R →* SignTypeˣ

              In case of an even dimension, the sign of the determinant of g : PGL(n, R) is well-defined.

              Instances For
                source
                📐 coverage
                theorem Matrix.ProjGenLinGroup.signDet_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) :
                signDet (mk g) = (Units.map ↑signHom) (GeneralLinearGroup.det g)
                source
                📐 coverage
                @[simp]
                theorem Matrix.ProjGenLinGroup.val_signDet_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) :
                ↑(signDet (mk g)) = SignType.sign ↑(GeneralLinearGroup.det g)