Lemmas about localizations of commutative monoids #
that requires additional imports.
theorem
Submonoid.IsLocalizationMap.surj_pi_of_finite
{M : Type u_1}
{N : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[Finite ι]
[CommMonoid M]
[CommMonoid N]
[FunLike F M N]
[MulHomClass F M N]
{f : F}
{S : Submonoid M}
(hf : S.IsLocalizationMap ⇑f)
(n : ι → N)
:
See also the analogous IsLocalization.map_integerMultiple.
theorem
AddSubmonoid.IsLocalizationMap.surj_pi_of_finite
{M : Type u_1}
{N : Type u_2}
{F : Type u_3}
{ι : Type u_4}
[Finite ι]
[AddCommMonoid M]
[AddCommMonoid N]
[FunLike F M N]
[AddHomClass F M N]
{f : F}
{S : AddSubmonoid M}
(hf : S.IsLocalizationMap ⇑f)
(n : ι → N)
:
theorem
Submonoid.IsLocalizationMap.pi
{ι : Type u_1}
{M : ι → Type u_2}
{N : ι → Type u_3}
[(i : ι) → CommMonoid (M i)]
[(i : ι) → CommMonoid (N i)]
(S : (i : ι) → Submonoid (M i))
{f : (i : ι) → M i → N i}
(hf : ∀ (i : ι), (S i).IsLocalizationMap (f i))
:
(pi Set.univ S).IsLocalizationMap (Pi.map f)
theorem
AddSubmonoid.IsLocalizationMap.pi
{ι : Type u_1}
{M : ι → Type u_2}
{N : ι → Type u_3}
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → AddCommMonoid (N i)]
(S : (i : ι) → AddSubmonoid (M i))
{f : (i : ι) → M i → N i}
(hf : ∀ (i : ι), (S i).IsLocalizationMap (f i))
:
(pi Set.univ S).IsLocalizationMap (Pi.map f)