Documentation

Mathlib.GroupTheory.FreeAbelianGroup

Free abelian groups #

The free abelian group on a type α, defined as the abelianisation of the free group on α.

The free abelian group on α can be abstractly defined as the left adjoint of the forgetful functor from abelian groups to types. Alternatively, one could define it as the functions α → ℤ which send all but finitely many (a : α) to 0, under pointwise addition. In this file, it is defined as the abelianisation of the free group on α. All the constructions and theorems required to show the adjointness of the construction and the forgetful functor are proved in this file, but the category-theoretic adjunction statement is in Algebra.Category.Group.Adjunctions.

Main definitions #

Here we use the following variables: (α β : Type*) (A : Type*) [AddCommGroup A]

It has been suggested that we would be better off refactoring this file and using Finsupp instead.

Implementation issues #

The definition is def FreeAbelianGroup : Type u := Additive <| Abelianization <| FreeGroup α.

Chris Hughes has suggested that this all be rewritten in terms of Finsupp. Johan Commelin has written all the API relating the definition to Finsupp in the lean-liquid repo.

The lemmas map_pure, map_of, map_zero, map_add, map_neg and map_sub are proved about the Functor.map <$> construction, and need α and β to be in the same universe. But FreeAbelianGroup.map (f : α → β) is defined to be the AddGroup homomorphism FreeAbelianGroup α →+ FreeAbelianGroup β (with α and β now allowed to be in different universes), so (map f).map_add etc can be used to prove that FreeAbelianGroup.map preserves addition. The functions map_id, map_id_apply, map_comp, map_comp_apply and map_of_apply are about FreeAbelianGroup.map.

def FreeAbelianGroup (α : Type u) :

The free abelian group on a type.

Equations
Instances For
    def FreeAbelianGroup.of {α : Type u} (x : α) :

    The canonical map from α to FreeAbelianGroup α.

    Equations
    Instances For
      def FreeAbelianGroup.lift {α : Type u} {β : Type v} [AddCommGroup β] :
      (αβ) (FreeAbelianGroup α →+ β)

      The map FreeAbelianGroup α →+ A induced by a map of types α → A.

      Equations
      • FreeAbelianGroup.lift = FreeGroup.lift.trans (Abelianization.lift.trans MonoidHom.toAdditive)
      Instances For
        @[simp]
        theorem FreeAbelianGroup.lift.of {α : Type u} {β : Type v} [AddCommGroup β] (f : αβ) (x : α) :
        (FreeAbelianGroup.lift f) (FreeAbelianGroup.of x) = f x
        theorem FreeAbelianGroup.lift.unique {α : Type u} {β : Type v} [AddCommGroup β] (f : αβ) (g : FreeAbelianGroup α →+ β) (hg : ∀ (x : α), g (FreeAbelianGroup.of x) = f x) {x : FreeAbelianGroup α} :
        g x = (FreeAbelianGroup.lift f) x
        theorem FreeAbelianGroup.lift.ext {α : Type u} {β : Type v} [AddCommGroup β] (g : FreeAbelianGroup α →+ β) (h : FreeAbelianGroup α →+ β) (H : ∀ (x : α), g (FreeAbelianGroup.of x) = h (FreeAbelianGroup.of x)) :
        g = h

        See note [partially-applied ext lemmas].

        theorem FreeAbelianGroup.lift.map_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : αβ) (g : β →+ γ) :
        g ((FreeAbelianGroup.lift f) a) = (FreeAbelianGroup.lift (g f)) a
        theorem FreeAbelianGroup.of_injective {α : Type u} :
        Function.Injective FreeAbelianGroup.of
        theorem FreeAbelianGroup.induction_on {α : Type u} {C : FreeAbelianGroup αProp} (z : FreeAbelianGroup α) (C0 : C 0) (C1 : ∀ (x : α), C (FreeAbelianGroup.of x)) (Cn : ∀ (x : α), C (FreeAbelianGroup.of x)C (-FreeAbelianGroup.of x)) (Cp : ∀ (x y : FreeAbelianGroup α), C xC yC (x + y)) :
        C z
        theorem FreeAbelianGroup.lift.add' {α : Type u_1} {β : Type u_2} [AddCommGroup β] (a : FreeAbelianGroup α) (f : αβ) (g : αβ) :
        (FreeAbelianGroup.lift (f + g)) a = (FreeAbelianGroup.lift f) a + (FreeAbelianGroup.lift g) a
        @[simp]
        theorem FreeAbelianGroup.liftAddGroupHom_apply {α : Type u_1} (β : Type u_2) [AddCommGroup β] (a : FreeAbelianGroup α) (f : αβ) :
        (FreeAbelianGroup.liftAddGroupHom β a) f = (FreeAbelianGroup.lift f) a
        def FreeAbelianGroup.liftAddGroupHom {α : Type u_1} (β : Type u_2) [AddCommGroup β] (a : FreeAbelianGroup α) :
        (αβ) →+ β

        If g : FreeAbelianGroup X and A is an abelian group then liftAddGroupHom g is the additive group homomorphism sending a function X → A to the term of type A corresponding to the evaluation of the induced map FreeAbelianGroup X → A at g.

        Equations
        Instances For
          theorem FreeAbelianGroup.lift_neg' {α : Type u} {β : Type u_1} [AddCommGroup β] (f : αβ) :
          FreeAbelianGroup.lift (-f) = -FreeAbelianGroup.lift f
          theorem FreeAbelianGroup.induction_on' {α : Type u} {C : FreeAbelianGroup αProp} (z : FreeAbelianGroup α) (C0 : C 0) (C1 : ∀ (x : α), C (pure x)) (Cn : ∀ (x : α), C (pure x)C (-pure x)) (Cp : ∀ (x y : FreeAbelianGroup α), C xC yC (x + y)) :
          C z
          @[simp]
          theorem FreeAbelianGroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
          f <$> pure x = pure (f x)
          @[simp]
          theorem FreeAbelianGroup.map_zero {α : Type u} {β : Type u} (f : αβ) :
          f <$> 0 = 0
          @[simp]
          theorem FreeAbelianGroup.map_add {α : Type u} {β : Type u} (f : αβ) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
          f <$> (x + y) = f <$> x + f <$> y
          @[simp]
          theorem FreeAbelianGroup.map_neg {α : Type u} {β : Type u} (f : αβ) (x : FreeAbelianGroup α) :
          f <$> (-x) = -f <$> x
          @[simp]
          theorem FreeAbelianGroup.map_sub {α : Type u} {β : Type u} (f : αβ) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
          f <$> (x - y) = f <$> x - f <$> y
          @[simp]
          theorem FreeAbelianGroup.map_of {α : Type u} {β : Type u} (f : αβ) (y : α) :
          theorem FreeAbelianGroup.pure_bind {α : Type u} {β : Type u} (f : αFreeAbelianGroup β) (x : α) :
          pure x >>= f = f x
          @[simp]
          theorem FreeAbelianGroup.zero_bind {α : Type u} {β : Type u} (f : αFreeAbelianGroup β) :
          0 >>= f = 0
          @[simp]
          theorem FreeAbelianGroup.add_bind {α : Type u} {β : Type u} (f : αFreeAbelianGroup β) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
          x + y >>= f = (x >>= f) + (y >>= f)
          @[simp]
          theorem FreeAbelianGroup.neg_bind {α : Type u} {β : Type u} (f : αFreeAbelianGroup β) (x : FreeAbelianGroup α) :
          -x >>= f = -(x >>= f)
          @[simp]
          theorem FreeAbelianGroup.sub_bind {α : Type u} {β : Type u} (f : αFreeAbelianGroup β) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
          x - y >>= f = (x >>= f) - (y >>= f)
          @[simp]
          theorem FreeAbelianGroup.pure_seq {α : Type u} {β : Type u} (f : αβ) (x : FreeAbelianGroup α) :
          (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
          @[simp]
          theorem FreeAbelianGroup.zero_seq {α : Type u} {β : Type u} (x : FreeAbelianGroup α) :
          (Seq.seq 0 fun (x_1 : Unit) => x) = 0
          @[simp]
          theorem FreeAbelianGroup.add_seq {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (g : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) :
          (Seq.seq (f + g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq g fun (x_1 : Unit) => x
          @[simp]
          theorem FreeAbelianGroup.neg_seq {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) :
          (Seq.seq (-f) fun (x_1 : Unit) => x) = -Seq.seq f fun (x_1 : Unit) => x
          @[simp]
          theorem FreeAbelianGroup.sub_seq {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (g : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) :
          (Seq.seq (f - g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) - Seq.seq g fun (x_1 : Unit) => x

          If f : FreeAbelianGroup (α → β), then f <*> is an additive morphism FreeAbelianGroup α →+ FreeAbelianGroup β.

          Equations
          Instances For
            @[simp]
            theorem FreeAbelianGroup.seq_zero {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) :
            (Seq.seq f fun (x : Unit) => 0) = 0
            @[simp]
            theorem FreeAbelianGroup.seq_add {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
            (Seq.seq f fun (x_1 : Unit) => x + y) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq f fun (x : Unit) => y
            @[simp]
            theorem FreeAbelianGroup.seq_neg {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) :
            (Seq.seq f fun (x_1 : Unit) => -x) = -Seq.seq f fun (x_1 : Unit) => x
            @[simp]
            theorem FreeAbelianGroup.seq_sub {α : Type u} {β : Type u} (f : FreeAbelianGroup (αβ)) (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
            (Seq.seq f fun (x_1 : Unit) => x - y) = (Seq.seq f fun (x_1 : Unit) => x) - Seq.seq f fun (x : Unit) => y
            def FreeAbelianGroup.map {α : Type u} {β : Type v} (f : αβ) :

            The additive group homomorphism FreeAbelianGroup α →+ FreeAbelianGroup β induced from a map α → β.

            Equations
            Instances For
              theorem FreeAbelianGroup.lift_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup γ] (f : αβ) (g : βγ) (x : FreeAbelianGroup α) :
              (FreeAbelianGroup.lift (g f)) x = (FreeAbelianGroup.lift g) ((FreeAbelianGroup.map f) x)
              theorem FreeAbelianGroup.map_comp {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : βγ} :
              theorem FreeAbelianGroup.map_comp_apply {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : βγ} (x : FreeAbelianGroup α) :
              @[simp]
              theorem FreeAbelianGroup.map_of_apply {α : Type u} {β : Type v} {f : αβ} (a : α) :
              instance FreeAbelianGroup.mul (α : Type u) [Mul α] :
              Equations
              theorem FreeAbelianGroup.mul_def {α : Type u} [Mul α] (x : FreeAbelianGroup α) (y : FreeAbelianGroup α) :
              x * y = (FreeAbelianGroup.lift fun (x₂ : α) => (FreeAbelianGroup.lift fun (x₁ : α) => FreeAbelianGroup.of (x₁ * x₂)) x) y
              @[simp]
              Equations
              Equations
              Equations
              Equations

              FreeAbelianGroup.of is a MonoidHom when α is a Monoid.

              Equations
              • FreeAbelianGroup.ofMulHom = { toFun := FreeAbelianGroup.of, map_one' := , map_mul' := }
              Instances For
                @[simp]
                theorem FreeAbelianGroup.ofMulHom_coe {α : Type u} [Monoid α] :
                FreeAbelianGroup.ofMulHom = FreeAbelianGroup.of
                def FreeAbelianGroup.liftMonoid {α : Type u} {R : Type u_1} [Monoid α] [Ring R] :

                If f preserves multiplication, then so does lift f.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem FreeAbelianGroup.liftMonoid_coe_addMonoidHom {α : Type u} {R : Type u_1} [Monoid α] [Ring R] (f : α →* R) :
                  (FreeAbelianGroup.liftMonoid f) = FreeAbelianGroup.lift f
                  @[simp]
                  theorem FreeAbelianGroup.liftMonoid_coe {α : Type u} {R : Type u_1} [Monoid α] [Ring R] (f : α →* R) :
                  (FreeAbelianGroup.liftMonoid f) = (FreeAbelianGroup.lift f)
                  @[simp]
                  theorem FreeAbelianGroup.liftMonoid_symm_coe {α : Type u} {R : Type u_1} [Monoid α] [Ring R] (f : FreeAbelianGroup α →+* R) :
                  (FreeAbelianGroup.liftMonoid.symm f) = FreeAbelianGroup.lift.symm f

                  The free abelian group on a type with one term is isomorphic to .

                  Equations
                  Instances For
                    def FreeAbelianGroup.equivOfEquiv {α : Type u_1} {β : Type u_2} (f : α β) :

                    Isomorphic types have isomorphic free abelian groups.

                    Equations
                    Instances For