Inverse_Completion_is_Unique
Provedinverse-completionsproofwikiuniqueness
The inverse completion of a commutative semigroup is unique up to isomorphism.
Preamble
import Mathlib.Algebra.Group.Equiv.Basic
Formal statement
theorem Inverse_Completion_is_Unique {S : Type _} [CommMonoid S] [IsCancelMul S] (G₁ G₂ : Type _) [CommGroup G₁] [CommGroup G₂] (f₁ : S →* G₁) (f₂ : S →* G₂) (hf₁ : Function.Injective f₁) (hf₂ : Function.Injective f₂) (hsurj₁ : ∀ g : G₁, ∃ a b : S, g = f₁ a * (f₁ b)⁻¹) (hsurj₂ : ∀ g : G₂, ∃ a b : S, g = f₂ a * (f₂ b)⁻¹) : Nonempty (G₁ ≃* G₂) := by sorrySource