mathlib docs: group_theory.free_abelian

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

source

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 := _}

source

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

source

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

source

theorem free_abelian_group.induction_on {α : Type u} {C : free_abelian_group α → Prop} (z : free_abelian_group α) (C0 : C 0) (C1 : ∀ (x : α), C (free_abelian_group.of x)) (Cn : ∀ (x : α), C (free_abelian_group.of x) → C (-free_abelian_group.of x)) (Cp : ∀ (x y : free_abelian_group α), C x → C y → C (x + y)) :

C z

source

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

source

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

source

@[instance]

def free_abelian_group.monad :

monad free_abelian_group

Equations

free_abelian_group.monad = monad.mk

source

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

C z

source

@[simp]

theorem free_abelian_group.map_pure {α β : Type u} (f : α → β) (x : α) :

f <$> pure x = pure (f x)

source

@[simp]

theorem free_abelian_group.map_zero {α β : Type u} (f : α → β) :

f <$> 0 = 0

source

@[simp]

theorem free_abelian_group.map_add {α β : Type u} (f : α → β) (x y : free_abelian_group α) :

f <$> (x + y) = f <$> x + f <$> y

source

@[simp]

theorem free_abelian_group.map_neg {α β : Type u} (f : α → β) (x : free_abelian_group α) :

f <$> -x = -f <$> x

source

@[simp]

theorem free_abelian_group.map_sub {α β : Type u} (f : α → β) (x y : free_abelian_group α) :

f <$> (x - y) = f <$> x - f <$> y

source

@[simp]

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

f <$> free_abelian_group.of y = free_abelian_group.of (f y)

source

def free_abelian_group.map {α β : Type u} (f : α → β) :

free_abelian_group α →+ free_abelian_group β

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) _

source

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)

source

@[simp]

theorem free_abelian_group.pure_bind {α β : Type u} (f : α → free_abelian_group β) (x : α) :

pure x >>= f = f x

source

@[simp]

theorem free_abelian_group.zero_bind {α β : Type u} (f : α → free_abelian_group β) :

0 >>= f = 0

source

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

source

@[simp]

theorem free_abelian_group.neg_bind {α β : Type u} (f : α → free_abelian_group β) (x : free_abelian_group α) :

-x >>= f = -(x >>= f)

source

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

source

@[simp]

theorem free_abelian_group.pure_seq {α β : Type u} (f : α → β) (x : free_abelian_group α) :

pure f <*> x = f <$> x

source

@[simp]

theorem free_abelian_group.zero_seq {α β : Type u} (x : free_abelian_group α) :

0 <*> x = 0

source

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

source

@[simp]

theorem free_abelian_group.neg_seq {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :

-f <*> x = -(f <*> x)

source

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

source

@[instance]

def free_abelian_group.is_add_group_hom_seq {α β : Type u} (f : free_abelian_group (α → β)) :

is_add_group_hom (has_seq.seq f)

source

@[simp]

theorem free_abelian_group.seq_zero {α β : Type u} (f : free_abelian_group (α → β)) :

f <*> 0 = 0

source

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

source

@[simp]

theorem free_abelian_group.seq_neg {α β : Type u} (f : free_abelian_group (α → β)) (x : free_abelian_group α) :

f <*> -x = -(f <*> x)

source

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

source

@[instance]

def free_abelian_group.is_lawful_monad :

is_lawful_monad free_abelian_group

source

@[instance]

def free_abelian_group.is_comm_applicative :

is_comm_applicative free_abelian_group

source

@[instance]

def free_abelian_group.semigroup (α : Type u) [monoid α] :

semigroup (free_abelian_group α)

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 := _}

source

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

source

theorem free_abelian_group.of_mul_of (α : Type u) [monoid α] (x y : α) :

(free_abelian_group.of x) * free_abelian_group.of y = free_abelian_group.of (x * y)

source

theorem free_abelian_group.of_mul (α : Type u) [monoid α] (x y : α) :

free_abelian_group.of (x * y) = (free_abelian_group.of x) * free_abelian_group.of y

source

@[instance]

def free_abelian_group.ring (α : Type u) [monoid α] :

ring (free_abelian_group α)

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 := _}

source

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

1 = free_abelian_group.of 1

source

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

free_abelian_group.of 1 = 1

source

@[instance]

def free_abelian_group.comm_ring (α : Type u) [comm_monoid α] :

comm_ring (free_abelian_group α)

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 := _}