Theorems · Definition · group theory

AddSubmonoid.LocalizationMap.ofAddEquivOfDom

{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} →
            [inst_2 : AddCommMonoid P] →
              S.LocalizationMap N →
                {T : AddSubmonoid P} → {k : P ≃+ M} → AddSubmonoid.map k.toAddMonoidHom T = S → T.LocalizationMap N

Given AddCommMonoids M, P and AddSubmonoids S ⊆ M, T ⊆ P, if f : M →* N is a Localization map for S and k : P ≃+ M is an isomorphism of AddCommMonoids such that k(T) = S, f ∘ k is a Localization map for T.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Maps

Cited by

6 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoidAddCommMonoidAddCommMonoid