Theorems · Theorem · group theory

Submonoid.LocalizationMap.mul_inv

∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S},
  f x₁ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₂)⁻¹ ↔
    f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Given a MonoidHom f : M →* N and Submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all x₁ x₂ : M and y₁, y₂ ∈ S, we have f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁).

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

3 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidCommMonoid