mathlib documentation

group_theory.free_abelian_group

def free_abelian_group  :
Type uType u

Equations
@[simp]
theorem free_abelian_group.lift.add {α : Type u} {β : Type v} [add_comm_group β] (f : α → β) (x y : free_abelian_group α) :

@[simp]
theorem free_abelian_group.lift.neg {α : Type u} {β : Type v} [add_comm_group β] (f : α → β) (x : free_abelian_group α) :

@[simp]
theorem free_abelian_group.lift.sub {α : Type u} {β : Type v} [add_comm_group β] (f : α → β) (x y : free_abelian_group α) :

@[simp]
theorem free_abelian_group.lift.zero {α : Type u} {β : Type v} [add_comm_group β] (f : α → β) :

@[simp]
theorem free_abelian_group.lift.of {α : Type u} {β : Type v} [add_comm_group β] (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 α} :

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 α} :
g x = h x

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 : β →+ γ) :

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
@[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) :

@[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) :

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 xC yC (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 : α → β) :

@[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)

theorem free_abelian_group.induction_on' {α : Type u} {C : free_abelian_group α → Prop} (z : free_abelian_group α) :
C 0(∀ (x : α), C (pure x))(∀ (x : α), C (pure x)C (-pure x))(∀ (x y : free_abelian_group α), C xC yC (x + y))C z

@[simp]
theorem free_abelian_group.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)

@[simp]
theorem free_abelian_group.map_zero {α β : Type u} (f : α → β) :
f <$> 0 = 0

@[simp]
theorem free_abelian_group.map_add {α β : Type u} (f : α → β) (x y : free_abelian_group α) :
f <$> (x + y) = f <$> x + f <$> y

@[simp]
theorem free_abelian_group.map_neg {α β : Type u} (f : α → β) (x : free_abelian_group α) :
f <$> -x = -f <$> x

@[simp]
theorem free_abelian_group.map_sub {α β : Type u} (f : α → β) (x y : free_abelian_group α) :
f <$> (x - y) = f <$> x - f <$> y

@[simp]
theorem free_abelian_group.map_of {α β : Type u} (f : α → β) (y : α) :

def free_abelian_group.map {α β : Type u} :

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

Equations
theorem free_abelian_group.lift_comp {α β : Type u_1} {γ : Type u_2} [add_comm_group γ] (f : α → β) (g : β → γ) (x : free_abelian_group α) :

@[simp]
theorem free_abelian_group.pure_bind {α β : Type u} (f : α → free_abelian_group β) (x : α) :
pure x >>= f = f x

@[simp]
theorem free_abelian_group.zero_bind {α β : Type u} (f : α → free_abelian_group β) :
0 >>= f = 0

@[simp]
theorem free_abelian_group.add_bind {α β : Type u} (f : α → free_abelian_group β) (x y : free_abelian_group α) :
x + y >>= f = (x >>= f) + (y >>= f)

@[simp]
theorem free_abelian_group.neg_bind {α β : Type u} (f : α → free_abelian_group β) (x : free_abelian_group α) :
-x >>= f = -(x >>= f)

@[simp]
theorem free_abelian_group.sub_bind {α β : Type u} (f : α → free_abelian_group β) (x y : free_abelian_group α) :
x - y >>= f = (x >>= f) - (y >>= f)

@[simp]
theorem free_abelian_group.pure_seq {α β : Type u} (f : α → β) (x : free_abelian_group α) :
pure f <*> x = f <$> x

@[simp]
theorem free_abelian_group.zero_seq {α β : Type u} (x : free_abelian_group α) :
0 <*> x = 0

@[simp]
theorem free_abelian_group.add_seq {α β : Type u} (f g : free_abelian_group (α → β)) (x : free_abelian_group α) :
f + g <*> x = (f <*> x) + (g <*> x)

@[simp]
theorem free_abelian_group.neg_seq {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :
-f <*> x = -(f <*> x)

@[simp]
theorem free_abelian_group.sub_seq {α β : Type u} (f g : free_abelian_group (α → β)) (x : free_abelian_group α) :
f - g <*> x = (f <*> x) - (g <*> x)

@[instance]

@[simp]
theorem free_abelian_group.seq_zero {α β : Type u} (f : free_abelian_group (α → β)) :
f <*> 0 = 0

@[simp]
theorem free_abelian_group.seq_add {α β : Type u} (f : free_abelian_group (α → β)) (x y : free_abelian_group α) :
f <*> x + y = (f <*> x) + (f <*> y)

@[simp]
theorem free_abelian_group.seq_neg {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :
f <*> -x = -(f <*> x)

@[simp]
theorem free_abelian_group.seq_sub {α β : Type u} (f : free_abelian_group (α → β)) (x y : free_abelian_group α) :
f <*> x - y = (f <*> x) - (f <*> y)

@[instance]

Equations
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

theorem free_abelian_group.one_def (α : Type u) [monoid α] :

theorem free_abelian_group.of_one (α : Type u) [monoid α] :