Equations
@[instance]
@[instance]
Equations
- free_abelian_group.inhabited α = {default := 0}
Equations
def
free_abelian_group.lift
{α : Type u}
{β : Type v}
[add_comm_group β] :
(α → β) → free_abelian_group α →+ β
Equations
@[simp]
theorem
free_abelian_group.lift.add
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β)
(x y : free_abelian_group α) :
⇑(free_abelian_group.lift f) (x + y) = ⇑(free_abelian_group.lift f) x + ⇑(free_abelian_group.lift f) y
@[simp]
theorem
free_abelian_group.lift.neg
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β)
(x : free_abelian_group α) :
⇑(free_abelian_group.lift f) (-x) = -⇑(free_abelian_group.lift f) x
@[simp]
theorem
free_abelian_group.lift.sub
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β)
(x y : free_abelian_group α) :
⇑(free_abelian_group.lift f) (x - y) = ⇑(free_abelian_group.lift f) x - ⇑(free_abelian_group.lift f) y
@[simp]
theorem
free_abelian_group.lift.zero
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β) :
⇑(free_abelian_group.lift f) 0 = 0
@[simp]
theorem
free_abelian_group.lift.of
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β)
(x : α) :
⇑(free_abelian_group.lift f) (free_abelian_group.of x) = f x
theorem
free_abelian_group.lift.unique
{α : Type u}
{β : Type v}
[add_comm_group β]
(f : α → β)
(g : free_abelian_group α →+ β)
(hg : ∀ (x : α), ⇑g (free_abelian_group.of x) = f x)
{x : free_abelian_group α} :
⇑g x = ⇑(free_abelian_group.lift f) x
theorem
free_abelian_group.lift.ext
{α : Type u}
{β : Type v}
[add_comm_group β]
(g h : free_abelian_group α →+ β)
(H : ∀ (x : α), ⇑g (free_abelian_group.of x) = ⇑h (free_abelian_group.of x))
{x : free_abelian_group α} :
theorem
free_abelian_group.lift.map_hom
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_group β]
[add_comm_group γ]
(a : free_abelian_group α)
(f : α → β)
(g : β →+ γ) :
⇑g (⇑(free_abelian_group.lift f) a) = ⇑(free_abelian_group.lift (⇑g ∘ f)) a
def
free_abelian_group.hom_equiv
(X : Type u_1)
(G : Type u_2)
[add_comm_group G] :
(free_abelian_group X →+ G) ≃ (X → G)
The bijection underlying the free-forgetful adjunction for abelian groups.
Equations
- free_abelian_group.hom_equiv X G = {to_fun := λ (f : free_abelian_group X →+ G), f.to_fun ∘ free_abelian_group.of, inv_fun := λ (f : X → G), add_monoid_hom.of ⇑(free_abelian_group.lift f), left_inv := _, right_inv := _}
@[simp]
theorem
free_abelian_group.hom_equiv_apply
(X : Type u_1)
(G : Type u_2)
[add_comm_group G]
(f : free_abelian_group X →+ G)
(x : X) :
⇑(free_abelian_group.hom_equiv X G) f x = ⇑f (free_abelian_group.of x)
@[simp]
theorem
free_abelian_group.hom_equiv_symm_apply
(X : Type u_1)
(G : Type u_2)
[add_comm_group G]
(f : X → G)
(x : free_abelian_group X) :
⇑(⇑((free_abelian_group.hom_equiv X G).symm) f) x = ⇑(free_abelian_group.lift f) x
theorem
free_abelian_group.induction_on
{α : Type u}
{C : free_abelian_group α → Prop}
(z : free_abelian_group α) :
C 0 → (∀ (x : α), C (free_abelian_group.of x)) → (∀ (x : α), C (free_abelian_group.of x) → C (-free_abelian_group.of x)) → (∀ (x y : free_abelian_group α), C x → C y → C (x + y)) → C z
theorem
free_abelian_group.lift.add'
{α : Type u_1}
{β : Type u_2}
[add_comm_group β]
(a : free_abelian_group α)
(f g : α → β) :
⇑(free_abelian_group.lift (f + g)) a = ⇑(free_abelian_group.lift f) a + ⇑(free_abelian_group.lift g) a
@[instance]
def
free_abelian_group.is_add_group_hom_lift'
{α : Type u_1}
(β : Type u_2)
[add_comm_group β]
(a : free_abelian_group α) :
is_add_group_hom (λ (f : α → β), ⇑(free_abelian_group.lift f) a)
Equations
@[instance]
Equations
theorem
free_abelian_group.induction_on'
{α : Type u}
{C : free_abelian_group α → Prop}
(z : free_abelian_group α) :
C 0 → (∀ (x : α), C (has_pure.pure x)) → (∀ (x : α), C (has_pure.pure x) → C (-has_pure.pure x)) → (∀ (x y : free_abelian_group α), C x → C y → C (x + y)) → C z
@[simp]
theorem
free_abelian_group.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
@[simp]
@[simp]
@[simp]
theorem
free_abelian_group.map_of
{α β : Type u}
(f : α → β)
(y : α) :
f <$> free_abelian_group.of y = free_abelian_group.of (f y)
The additive group homomorphism free_abelian_group α →+ free_abelian_group β induced from a
map α → β
Equations
- free_abelian_group.map f = add_monoid_hom.mk' (λ (x : free_abelian_group α), f <$> x) _
theorem
free_abelian_group.lift_comp
{α β : Type u_1}
{γ : Type u_2}
[add_comm_group γ]
(f : α → β)
(g : β → γ)
(x : free_abelian_group α) :
⇑(free_abelian_group.lift (g ∘ f)) x = ⇑(free_abelian_group.lift g) (f <$> x)
@[simp]
theorem
free_abelian_group.pure_bind
{α β : Type u}
(f : α → free_abelian_group β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
@[simp]
theorem
free_abelian_group.add_bind
{α β : Type u}
(f : α → free_abelian_group β)
(x y : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.neg_bind
{α β : Type u}
(f : α → free_abelian_group β)
(x : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.sub_bind
{α β : Type u}
(f : α → free_abelian_group β)
(x y : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.pure_seq
{α β : Type u}
(f : α → β)
(x : free_abelian_group α) :
has_pure.pure f <*> x = f <$> x
@[simp]
@[simp]
theorem
free_abelian_group.add_seq
{α β : Type u}
(f g : free_abelian_group (α → β))
(x : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.neg_seq
{α β : Type u}
(f : free_abelian_group (α → β))
(x : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.sub_seq
{α β : Type u}
(f g : free_abelian_group (α → β))
(x : free_abelian_group α) :
@[instance]
Equations
@[simp]
@[simp]
theorem
free_abelian_group.seq_add
{α β : Type u}
(f : free_abelian_group (α → β))
(x y : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.seq_neg
{α β : Type u}
(f : free_abelian_group (α → β))
(x : free_abelian_group α) :
@[simp]
theorem
free_abelian_group.seq_sub
{α β : Type u}
(f : free_abelian_group (α → β))
(x y : free_abelian_group α) :
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
- free_abelian_group.semigroup α = {mul := λ (x : free_abelian_group α), ⇑(free_abelian_group.lift (λ (x₂ : α), ⇑(free_abelian_group.lift (λ (x₁ : α), free_abelian_group.of (x₁ * x₂))) x)), mul_assoc := _}
theorem
free_abelian_group.mul_def
(α : Type u)
[monoid α]
(x y : free_abelian_group α) :
x * y = ⇑(free_abelian_group.lift (λ (x₂ : α), ⇑(free_abelian_group.lift (λ (x₁ : α), free_abelian_group.of (x₁ * x₂))) x)) y
@[instance]
Equations
- free_abelian_group.ring α = {add := add_comm_group.add (free_abelian_group.add_comm_group α), add_assoc := _, zero := add_comm_group.zero (free_abelian_group.add_comm_group α), zero_add := _, add_zero := _, neg := add_comm_group.neg (free_abelian_group.add_comm_group α), add_left_neg := _, add_comm := _, mul := semigroup.mul (free_abelian_group.semigroup α), mul_assoc := _, one := free_abelian_group.of 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[instance]
Equations
- free_abelian_group.comm_ring α = {add := ring.add (free_abelian_group.ring α), add_assoc := _, zero := ring.zero (free_abelian_group.ring α), zero_add := _, add_zero := _, neg := ring.neg (free_abelian_group.ring α), add_left_neg := _, add_comm := _, mul := ring.mul (free_abelian_group.ring α), mul_assoc := _, one := ring.one (free_abelian_group.ring α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}