FreeAbelianGroup.map_comp_apply
theorem FreeAbelianGroup.map_comp_apply :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} (x : FreeAbelianGroup α),
(FreeAbelianGroup.map (g ∘ f)) x = (FreeAbelianGroup.map g) ((FreeAbelianGroup.map f) x)
The theorem `FreeAbelianGroup.map_comp_apply` states that for any types `α`, `β`, and `γ`, and any functions `f` from `α` to `β` and `g` from `β` to `γ`, the map induced by the composition of `f` and `g` on the free abelian group generated by `α` is equivalent to first applying the map induced by `f` and then applying the map induced by `g`. This is essentially a statement of functoriality of the free abelian group construction in the category of types and functions. It is a formalized version of the mathematical principle that composition of functions is associative in the context of free abelian groups.
More concisely: The map induced by the composition of two functions between types is equal to the composition of the induced maps on the free abelian groups generated by those types.
|
FreeAbelianGroup.of_mul_of
theorem FreeAbelianGroup.of_mul_of :
∀ {α : Type u} [inst : Mul α] (x y : α),
FreeAbelianGroup.of x * FreeAbelianGroup.of y = FreeAbelianGroup.of (x * y)
This theorem states that for any type `α` with a multiplication operation, and any elements `x` and `y` of type `α`, the product of the canonical map applied to `x` and `y` in the `FreeAbelianGroup` of `α` is equal to the canonical map applied to the product of `x` and `y`. In more mathematical terms, it asserts that the canonical map `FreeAbelianGroup.of` preserves the multiplication operation from `α` to its Free Abelian Group.
More concisely: For any type `α` with a multiplication operation and any elements `x` and `y` of type `α`, the canonical map from `α` to its Free Abelian Group maps `(x * y)` to `(FreeAbelianGroup.of x) * (FreeAbelianGroup.of y)`.
|
FreeAbelianGroup.induction_on
theorem FreeAbelianGroup.induction_on :
∀ {α : Type u} {C : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α),
C 0 →
(∀ (x : α), C (FreeAbelianGroup.of x)) →
(∀ (x : α), C (FreeAbelianGroup.of x) → C (-FreeAbelianGroup.of x)) →
(∀ (x y : FreeAbelianGroup α), C x → C y → C (x + y)) → C z
This theorem, called `FreeAbelianGroup.induction_on`, states that for any type `α` and any property `C` that holds for elements of the free Abelian group on `α`, if `C` holds for the zero element, for any element of `α` mapped into the free Abelian group, for the additive inverse of any such element, and is closed under addition in the free Abelian group (i.e., if it holds for any two elements, it also holds for their sum), then `C` holds for every element of the free Abelian group. This theorem provides a principle of induction for proving properties over all elements of the free Abelian group.
More concisely: If a property `C` holds for the zero element and is closed under addition in a free Abelian group, then `C` holds for all elements if it holds for each element and its additive inverse.
|
FreeAbelianGroup.lift.ext
theorem FreeAbelianGroup.lift.ext :
∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (g h : FreeAbelianGroup α →+ β),
(∀ (x : α), g (FreeAbelianGroup.of x) = h (FreeAbelianGroup.of x)) → g = h
This theorem, `FreeAbelianGroup.lift.ext`, states that for any two homomorphisms `g` and `h` from the free abelian group on a type `α` to an additive commutative group `β`, if `g` and `h` agree on the image under the canonical map `FreeAbelianGroup.of` of every element of `α`, then `g` and `h` are equal. In other words, it's saying that to define a group homomorphism out of the free abelian group, it's enough to specify where the generators (the images under `FreeAbelianGroup.of` of elements of `α`) should go, and this definition is uniquely determining the homomorphism.
More concisely: Given two homomorphisms from a free abelian group to an additive commutative group that agree on the images of generators, they are equal.
|
FreeAbelianGroup.lift.of
theorem FreeAbelianGroup.lift.of :
∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (f : α → β) (x : α),
(FreeAbelianGroup.lift f) (FreeAbelianGroup.of x) = f x
The theorem `FreeAbelianGroup.lift.of` states that for any type `α` and `β`, where `β` is an instance of an additive commutative group, and for any function `f` from `α` to `β`, and any element `x` of type `α`, the result of lifting `f` through the free abelian group of `α` and then applying it to the canonical map from `α` to its free abelian group applied to `x` is equal to directly applying `f` to `x`. This effectively asserts the compatibility of the lift operation with the canonical embedding into the free abelian group.
More concisely: Given a type `α`, an additive commutative group `β`, and a function `f` from `α` to `β`, the lifted application of `f` to the free abelian group element represented by `x` in `α` equals the direct application of `f` to `x`.
|
FreeAbelianGroup.map_add
theorem FreeAbelianGroup.map_add :
∀ {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α), f <$> (x + y) = f <$> x + f <$> y
The `FreeAbelianGroup.map_add` theorem states that for any types `α` and `β`, and a function `f` from `α` to `β`, the action of `f` on the sum of two elements `x` and `y` in the free abelian group over `α` is the same as the sum of the action of `f` on `x` and `y` separately. In other words, this theorem shows that the function `f` preserves the addition operation when mapped over elements in the free abelian group, a property known as additivity. This could be expressed in mathematical notation as follows: for all `f : α → β` and `x, y` in the free abelian group on `α`, `f(x + y) = f(x) + f(y)`.
More concisely: For any function `f` from a type `α` to a type `β` and any elements `x, y` in the free abelian group on `α`, `f(x + y) = f(x) + f(y)`.
|
FreeAbelianGroup.map_id
theorem FreeAbelianGroup.map_id : ∀ {α : Type u}, FreeAbelianGroup.map id = AddMonoidHom.id (FreeAbelianGroup α) := by
sorry
The theorem `FreeAbelianGroup.map_id` asserts that for any type `α`, applying the identity function as the map in `FreeAbelianGroup.map` results in the same homomorphism as `AddMonoidHom.id` (the identity map) on the type `FreeAbelianGroup α`. In other words, the homomorphism induced by the identity function in the context of free abelian groups is, indeed, the identity homomorphism.
More concisely: The identity function induces the identity homomorphism in the context of FreeAbelianGroups.
|