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)
:
∃ (s : ↥S) (x : ι → M), ∀ (i : ι), n i * f ↑s = f (x i)
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)
:
∃ (s : ↥S) (x : ι → M), ∀ (i : ι), n i + f ↑s = f (x i)
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)