Documentation

TauCeti.GroupTheory.SpecificGroups.Affine.Basic

One-dimensional affine groups #

For a ring F, the one-dimensional affine group is the semidirect product of the additive group of F by its unit group. We realize the additive group as Multiplicative F, so that Mathlib's multiplicative semidirect product can be used directly. An element (b, a) acts on F by x ↦ b + a * x.

This file identifies the translation and linear-factor subgroups and proves that they are complementary, all over an arbitrary ring. Over a ring without zero divisors, every nonidentity linear factor acts without nonidentity fixed points on the translations. Over a division ring it also computes the cardinalities of the two factors. Thus finite affine groups with at least three elements are Frobenius groups; their Frobenius kernels are identified in TauCeti.RepresentationTheory.FrobeniusGroup.Affine.

Main definitions and results #

The construction is the standard affine-group example; see Isaacs, Character Theory of Finite Groups, Chapter 7.

source
def TauCeti.affineAction (F : Type u_1) [Ring F] :
Fˣ →* MulAut (Multiplicative F)

Multiplication by units, regarded as automorphisms of the additive group of a ring.

Instances For
    source
    @[simp]
    theorem TauCeti.affineAction_apply_toAdd {F : Type u_1} [Ring F] (u : Fˣ) (x : Multiplicative F) :
    Multiplicative.toAdd (((affineAction F) u) x) = ↑u * Multiplicative.toAdd x
    source
    @[reducible, inline]
    abbrev TauCeti.AffineGroup (F : Type u_1) [Ring F] :
    Type u_1

    The one-dimensional affine group F ⋊ Fˣ, with units acting on the additive group by multiplication.

    Instances For
      source
      instance TauCeti.instFiniteAffineGroup {F : Type u_1} [Ring F] [Finite F] :
      Finite (AffineGroup F)

      A one-dimensional affine group over a finite ring is finite.

      source
      @[instance_reducible]
      instance TauCeti.instSMulAffineGroup {F : Type u_1} [Ring F] :
      SMul (AffineGroup F) F

      An element (b, a) of the affine group sends x to b + a * x.

      source
      theorem TauCeti.AffineGroup.smul_def {F : Type u_1} [Ring F] (g : AffineGroup F) (x : F) :
      g • x = Multiplicative.toAdd g.left + ↑g.right * x

      An element (b, a) of the affine group acts by x ↦ b + a * x.

      source
      @[instance_reducible]
      instance TauCeti.instMulActionAffineGroup {F : Type u_1} [Ring F] :
      MulAction (AffineGroup F) F

      The affine group acts on its ring by affine maps.

      source
      instance TauCeti.instFaithfulSMulAffineGroup {F : Type u_1} [Ring F] :
      FaithfulSMul (AffineGroup F) F

      The affine group acts faithfully on its ring: an affine map is determined by its values at 0 and 1.

      source
      def TauCeti.affineTranslationSubgroup (F : Type u_1) [Ring F] :
      Subgroup (AffineGroup F)

      The normal subgroup of translations in the affine group.

      Instances For
        source
        def TauCeti.affineLinearSubgroup (F : Type u_1) [Ring F] :
        Subgroup (AffineGroup F)

        The subgroup of linear maps fixing zero in the affine group.

        Instances For
          source
          @[simp]
          theorem TauCeti.mem_affineTranslationSubgroup_iff {F : Type u_1} [Ring F] (g : AffineGroup F) :
          g ∈ affineTranslationSubgroup F ↔ g.right = 1

          An affine transformation is a translation exactly when its linear coordinate is one.

          source
          @[simp]
          theorem TauCeti.mem_affineLinearSubgroup_iff {F : Type u_1} [Ring F] (g : AffineGroup F) :
          g ∈ affineLinearSubgroup F ↔ Multiplicative.toAdd g.left = 0

          An affine transformation lies in the linear factor exactly when its translation coordinate is zero.

          source
          instance TauCeti.instNormalAffineGroupAffineTranslationSubgroup {F : Type u_1} [Ring F] :
          (affineTranslationSubgroup F).Normal

          The translation subgroup of an affine group is normal.

          source
          theorem TauCeti.isComplement'_affineTranslationSubgroup_affineLinearSubgroup (F : Type u_1) [Ring F] :
          (affineTranslationSubgroup F).IsComplement' (affineLinearSubgroup F)

          The translation and linear-factor subgroups of an affine group are complementary.

          source
          theorem TauCeti.card_affineTranslationSubgroup (F : Type u_1) [Ring F] :
          Nat.card ↥(affineTranslationSubgroup F) = Nat.card F

          The translation subgroup of an affine group has the same natural cardinality as the ring.

          source
          theorem TauCeti.card_affineLinearSubgroup (F : Type u_1) [DivisionRing F] :
          Nat.card ↥(affineLinearSubgroup F) = Nat.card F - 1

          The linear factor of an affine group has natural cardinality one less than the ring.

          source
          theorem TauCeti.card_affineGroup (F : Type u_1) [DivisionRing F] :
          Nat.card (AffineGroup F) = Nat.card F * (Nat.card F - 1)

          A one-dimensional affine group has natural cardinality |F| (|F| - 1).

          source
          theorem TauCeti.fixedPointFree_conjNormal_affineTranslationSubgroup {F : Type u_1} [Ring F] [NoZeroDivisors F] (h : ↥(affineLinearSubgroup F)) (hh : h ≠ 1) :
          MonoidHom.FixedPointFree ⇑(MulAut.conjNormal ↑h)

          A nonidentity element of the linear factor acts without nonidentity fixed points on the translation subgroup.

          source
          theorem TauCeti.isTISubgroup_affineLinearSubgroup (F : Type u_1) [Ring F] [NoZeroDivisors F] :
          IsTISubgroup (affineLinearSubgroup F)

          The linear factor in an affine group is a trivial-intersection subgroup.

          source
          theorem TauCeti.isFrobeniusComplement_affineLinearSubgroup (F : Type u_1) [DivisionRing F] (hF : 3 ≤ Nat.card F) :
          IsFrobeniusComplement (affineLinearSubgroup F)

          For a finite division ring of order at least three, its affine group is a Frobenius group with the linear factor as a Frobenius complement.