Associated elements. #

In this file we define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient.

source

def Associated {M : Type u_1} [Monoid M] (x y : M) :

Prop

Two elements of a Monoid are Associated if one of them is another one multiplied by a unit on the right.

Equations

Associated x y = ∃ (u : M ˣ ), x * ↑u = y

source

theorem Associated.refl {M : Type u_1} [Monoid M] (x : M) :

Associated x x

source

theorem Associated.rfl {M : Type u_1} [Monoid M] {x : M} :

Associated x x

source

instance Associated.instIsRefl {M : Type u_1} [Monoid M] :

IsRefl M Associated

source

theorem Associated.symm {M : Type u_1} [Monoid M] {x y : M} :

Associated x y → Associated y x

source

instance Associated.instIsSymm {M : Type u_1} [Monoid M] :

IsSymm M Associated

source

theorem Associated.comm {M : Type u_1} [Monoid M] {x y : M} :

Associated x y ↔ Associated y x

source

theorem Associated.trans {M : Type u_1} [Monoid M] {x y z : M} :

Associated x y → Associated y z → Associated x z

source

instance Associated.instIsTrans {M : Type u_1} [Monoid M] :

IsTrans M Associated

source

def Associated.setoid (M : Type u_2) [Monoid M] :

Setoid M

The setoid of the relation x ~ᵤ y iff there is a unit u such that x * u = y

Equations

Associated.setoid M = { r := Associated, iseqv := ⋯ }

source

theorem Associated.map {M : Type u_2} {N : Type u_3} [Monoid M] [Monoid N] {F : Type u_4} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x y : M} (ha : Associated x y) :

Associated (f x) (f y)

source

theorem unit_associated_one {M : Type u_1} [Monoid M] {u : M ˣ} :

Associated (↑u) 1

source

@[simp]

theorem associated_one_iff_isUnit {M : Type u_1} [Monoid M] {a : M} :

Associated a 1 ↔ IsUnit a

source

@[simp]

theorem associated_zero_iff_eq_zero {M : Type u_1} [MonoidWithZero M] (a : M) :

Associated a 0 ↔ a = 0

source

theorem associated_one_of_mul_eq_one {M : Type u_1} [CommMonoid M] {a : M} (b : M) (hab : a * b = 1) :

Associated a 1

source

theorem associated_one_of_associated_mul_one {M : Type u_1} [CommMonoid M] {a b : M} :

Associated (a * b) 1 → Associated a 1

source

theorem associated_mul_unit_left {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :

Associated (a * u) a

source

theorem associated_unit_mul_left {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :

Associated (u * a) a

source

theorem associated_mul_unit_right {N : Type u_2} [Monoid N] (a u : N) (hu : IsUnit u) :

Associated a (a * u)

source

theorem associated_unit_mul_right {N : Type u_2} [CommMonoid N] (a u : N) (hu : IsUnit u) :

Associated a (u * a)

source

theorem associated_mul_isUnit_left_iff {N : Type u_2} [Monoid N] {a u b : N} (hu : IsUnit u) :

Associated (a * u) b ↔ Associated a b

source

theorem associated_isUnit_mul_left_iff {N : Type u_2} [CommMonoid N] {u a b : N} (hu : IsUnit u) :

Associated (u * a) b ↔ Associated a b

source

theorem associated_mul_isUnit_right_iff {N : Type u_2} [Monoid N] {a b u : N} (hu : IsUnit u) :

Associated a (b * u) ↔ Associated a b

source

theorem associated_isUnit_mul_right_iff {N : Type u_2} [CommMonoid N] {a u b : N} (hu : IsUnit u) :

Associated a (u * b) ↔ Associated a b

source

@[simp]

theorem associated_mul_unit_left_iff {N : Type u_2} [Monoid N] {a b : N} {u : N ˣ} :

Associated (a * ↑u) b ↔ Associated a b

source

@[simp]

theorem associated_unit_mul_left_iff {N : Type u_2} [CommMonoid N] {a b : N} {u : N ˣ} :

Associated (↑u * a) b ↔ Associated a b

source

@[simp]

theorem associated_mul_unit_right_iff {N : Type u_2} [Monoid N] {a b : N} {u : N ˣ} :

Associated a (b * ↑u) ↔ Associated a b

source

@[simp]

theorem associated_unit_mul_right_iff {N : Type u_2} [CommMonoid N] {a b : N} {u : N ˣ} :

Associated a (↑u * b) ↔ Associated a b

source

theorem Associated.mul_left {M : Type u_1} [Monoid M] (a : M) {b c : M} (h : Associated b c) :

Associated (a * b) (a * c)

source

theorem Associated.mul_right {M : Type u_1} [CommMonoid M] {a b : M} (h : Associated a b) (c : M) :

Associated (a * c) (b * c)

source

theorem Associated.mul_mul {M : Type u_1} [CommMonoid M] {a₁ a₂ b₁ b₂ : M} (h₁ : Associated a₁ b₁) (h₂ : Associated a₂ b₂) :

Associated (a₁ * a₂) (b₁ * b₂)

source

theorem Associated.pow_pow {M : Type u_1} [CommMonoid M] {a b : M} {n : ℕ} (h : Associated a b) :

Associated (a ^ n) (b ^ n)

source

theorem Associated.dvd {M : Type u_1} [Monoid M] {a b : M} :

Associated a b → a ∣ b

source

theorem Associated.dvd' {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :

b ∣ a

source

theorem Associated.dvd_dvd {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :

a ∣ b ∧ b ∣ a

source

theorem associated_of_dvd_dvd {M : Type u_1} [CancelMonoidWithZero M] {a b : M} (hab : a ∣ b) (hba : b ∣ a) :

Associated a b

source

theorem dvd_dvd_iff_associated {M : Type u_1} [CancelMonoidWithZero M] {a b : M} :

a ∣ b ∧ b ∣ a ↔ Associated a b

source

instance instDecidableRelAssociatedOfDvd {M : Type u_1} [CancelMonoidWithZero M] [DecidableRel fun (x1 x2 : M) => x1 ∣ x2] :

DecidableRel fun (x1 x2 : M) => Associated x1 x2

Equations

instDecidableRelAssociatedOfDvd x✝¹ x✝ = decidable_of_iff (x✝¹ ∣ x✝ ∧ x✝ ∣ x✝¹) ⋯

source

theorem Associated.dvd_iff_dvd_left {M : Type u_1} [Monoid M] {a b c : M} (h : Associated a b) :

a ∣ c ↔ b ∣ c

source

theorem Associated.dvd_iff_dvd_right {M : Type u_1} [Monoid M] {a b c : M} (h : Associated b c) :

a ∣ b ↔ a ∣ c

source

theorem Associated.eq_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :

a = 0 ↔ b = 0

source

theorem Associated.ne_zero_iff {M : Type u_1} [MonoidWithZero M] {a b : M} (h : Associated a b) :

a ≠ 0 ↔ b ≠ 0

source

theorem Associated.prime {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) (hp : Prime p) :

Prime q

source

theorem prime_mul_iff {M : Type u_1} [CancelCommMonoidWithZero M] {x y : M} :

Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

source

@[simp]

theorem prime_pow_iff {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} {n : ℕ} :

Prime (p ^ n) ↔ Prime p ∧ n = 1

source

theorem Irreducible.dvd_iff {M : Type u_1} [Monoid M] {x y : M} (hx : Irreducible x) :

y ∣ x ↔ IsUnit y ∨ Associated x y

source

theorem Irreducible.associated_of_dvd {M : Type u_1} [Monoid M] {p q : M} (p_irr : Irreducible p) (q_irr : Irreducible q) (dvd : p ∣ q) :

Associated p q

source

theorem Irreducible.dvd_irreducible_iff_associated {M : Type u_1} [Monoid M] {p q : M} (pp : Irreducible p) (qp : Irreducible q) :

p ∣ q ↔ Associated p q

source

theorem Prime.associated_of_dvd {M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (p_prime : Prime p) (q_prime : Prime q) (dvd : p ∣ q) :

Associated p q

source

theorem Prime.dvd_prime_iff_associated {M : Type u_1} [CancelCommMonoidWithZero M] {p q : M} (pp : Prime p) (qp : Prime q) :

p ∣ q ↔ Associated p q

source

theorem Associated.prime_iff {M : Type u_1} [CommMonoidWithZero M] {p q : M} (h : Associated p q) :

Prime p ↔ Prime q

source

theorem Associated.isUnit {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :

IsUnit a → IsUnit b

source

theorem Associated.isUnit_iff {M : Type u_1} [Monoid M] {a b : M} (h : Associated a b) :

IsUnit a ↔ IsUnit b

source

theorem Irreducible.isUnit_iff_not_associated_of_dvd {M : Type u_1} [Monoid M] {x y : M} (hx : Irreducible x) (hy : y ∣ x) :

IsUnit y ↔ ¬Associated x y

source

theorem Associated.irreducible {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) (hp : Irreducible p) :

Irreducible q

source

theorem Associated.irreducible_iff {M : Type u_1} [Monoid M] {p q : M} (h : Associated p q) :

Irreducible p ↔ Irreducible q

source

theorem Associated.of_mul_left {M : Type u_1} [CancelCommMonoidWithZero M] {a b c d : M} (h : Associated (a * b) (c * d)) (h₁ : Associated a c) (ha : a ≠ 0) :

Associated b d

source

theorem Associated.of_mul_right {M : Type u_1} [CancelCommMonoidWithZero M] {a b c d : M} :

Associated (a * b) (c * d) → Associated b d → b ≠ 0 → Associated a c

source

theorem Associated.of_pow_associated_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : Associated (p₁ ^ k₁) (p₂ ^ k₂)) :

Associated p₁ p₂

source

theorem Associated.of_pow_associated_of_prime' {M : Type u_1} [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₂ : 0 < k₂) (h : Associated (p₁ ^ k₁) (p₂ ^ k₂)) :

Associated p₁ p₂

source

theorem Irreducible.isRelPrime_iff_not_dvd {M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) :

IsRelPrime p n ↔ ¬p ∣ n

See also Irreducible.coprime_iff_not_dvd.

source

theorem Irreducible.dvd_or_isRelPrime {M : Type u_1} [Monoid M] {p n : M} (hp : Irreducible p) :

p ∣ n ∨ IsRelPrime p n

source

theorem associated_iff_eq {M : Type u_1} [Monoid M] [Subsingleton M ˣ] {x y : M} :

Associated x y ↔ x = y

source

theorem associated_eq_eq {M : Type u_1} [Monoid M] [Subsingleton M ˣ] :

Associated = Eq

source

theorem prime_dvd_prime_iff_eq {M : Type u_2} [CancelCommMonoidWithZero M] [Subsingleton M ˣ] {p q : M} (pp : Prime p) (qp : Prime q) :

p ∣ q ↔ p = q

source

theorem eq_of_prime_pow_eq {R : Type u_2} [CancelCommMonoidWithZero R] [Subsingleton R ˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :

p₁ = p₂

source

theorem eq_of_prime_pow_eq' {R : Type u_2} [CancelCommMonoidWithZero R] [Subsingleton R ˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ} (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :

p₁ = p₂

source

@[reducible, inline]

abbrev Associates (M : Type u_2) [Monoid M] :

Type u_2

The quotient of a monoid by the Associated relation. Two elements x and y are associated iff there is a unit u such that x * u = y. There is a natural monoid structure on Associates M.

Equations