theorem
zero_mem_nonZeroDivisors
{M : Type u_1}
[MonoidWithZero M]
[Subsingleton M]
:
0 ∈ nonZeroDivisors M
theorem
IsLocalizedModule.mk'_right_smul_mk'
{R : Type u_1}
{M : Type u_2}
{S_M : Type u_3}
(S_R : Type u_4)
[CommSemiring R]
[CommSemiring S_R]
[Algebra R S_R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
(m : M)
(s : ↥S)
(t : ↥S)
:
IsLocalization.mk' S_R 1 s • IsLocalizedModule.mk' f m t = IsLocalizedModule.mk' f m (s * t)
theorem
IsLocalizedModule.mk'_right_smul_mk'_left
{R : Type u_1}
{M : Type u_2}
{S_M : Type u_3}
(S_R : Type u_4)
[CommSemiring R]
[CommSemiring S_R]
[Algebra R S_R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
(m : M)
(s : ↥S)
:
IsLocalization.mk' S_R 1 s • f m = IsLocalizedModule.mk' f m s
theorem
Submodule.localized'_comap_eq
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
(S_p : Submodule S_R S_M)
:
Submodule.localized' S_R S f (Submodule.comap f (Submodule.restrictScalars R S_p)) = S_p
theorem
Submodule.localized'_mono
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
{p : Submodule R M}
{q : Submodule R M}
:
p ≤ q → Submodule.localized' S_R S f p ≤ Submodule.localized' S_R S f q
def
Submodule.localized'OrderEmbedding
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
:
Equations
- Submodule.localized'OrderEmbedding S_R S f = { toFun := fun (S_p : Submodule S_R S_M) => Submodule.comap f (Submodule.restrictScalars R S_p), inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
theorem
Submodule.localized'_of_trivial
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
{p : Submodule R M}
(h : 0 ∈ S)
:
Submodule.localized' S_R S f p = ⊤
theorem
Submodule.localized'_sup
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
{p : Submodule R M}
{q : Submodule R M}
:
Submodule.localized' S_R S f (p ⊔ q) = Submodule.localized' S_R S f p ⊔ Submodule.localized' S_R S f q
theorem
Submodule.localized'_inf
{R : Type u_5}
{M : Type u_6}
{S_M : Type u_7}
(S_R : Type u_8)
[CommRing R]
[CommRing S_R]
[Algebra R S_R]
[AddCommGroup M]
[Module R M]
[AddCommGroup S_M]
[Module R S_M]
[Module S_R S_M]
[IsScalarTower R S_R S_M]
(S : Submonoid R)
[IsLocalization S S_R]
(f : M →ₗ[R] S_M)
[IsLocalizedModule S f]
{p : Submodule R M}
{q : Submodule R M}
:
Submodule.localized' S_R S f (p ⊓ q) = Submodule.localized' S_R S f p ⊓ Submodule.localized' S_R S f q
theorem
Submodule.localized_of_trivial
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
{p : Submodule R M}
(h : 0 ∈ S)
:
Submodule.localized S p = ⊤
theorem
Submodule.localized_bot
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
:
theorem
Submodule.localized_top
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
:
theorem
Submodule.localized_sup
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
{p : Submodule R M}
{q : Submodule R M}
:
Submodule.localized S (p ⊔ q) = Submodule.localized S p ⊔ Submodule.localized S q
theorem
Submodule.localized_inf
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
{p : Submodule R M}
{q : Submodule R M}
:
Submodule.localized S (p ⊓ q) = Submodule.localized S p ⊓ Submodule.localized S q
theorem
Submodule.localized_span
{R : Type u_5}
{M : Type u_6}
[CommRing R]
[AddCommGroup M]
[Module R M]
(S : Submonoid R)
(s : Set M)
:
Submodule.localized S (Submodule.span R s) = Submodule.span (Localization S) (⇑(LocalizedModule.mkLinearMap S M) '' s)