theorem
injective_of_localization
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Function.Injective ⇑((map' J.primeCompl) f))
:
theorem
surjective_of_localization
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Function.Surjective ⇑((map' J.primeCompl) f))
:
theorem
bijective_of_localization
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f))
:
noncomputable def
linearEquivOfLocalization
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f))
:
Equations
Instances For
theorem
linearEquivOfLocalization_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Function.Bijective ⇑((map' J.primeCompl) f))
(m : M)
:
(linearEquivOfLocalization f h) m = f m
theorem
localization_injective
{R : Type u_4}
{S : Type u_5}
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Submonoid R)
[IsLocalization p S]
{M : Type u_6}
{N : Type u_7}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
{P : Type u_8}
{Q : Type u_9}
[AddCommGroup P]
[Module R P]
[AddCommGroup Q]
[Module R Q]
[Module S Q]
[IsScalarTower R S Q]
(f' : P →ₗ[R] Q)
[IsLocalizedModule p f']
{g : M →ₗ[R] P}
(h : Function.Injective ⇑g)
:
Function.Injective ⇑(LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))
theorem
injective_localizationPreserves
{R : Type u_4}
[CommRing R]
(p : Submonoid R)
{M : Type u_6}
{N : Type u_7}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
{P : Type u_8}
{Q : Type u_9}
[AddCommGroup P]
[Module R P]
[AddCommGroup Q]
[Module R Q]
(f' : P →ₗ[R] Q)
[IsLocalizedModule p f']
{g : M →ₗ[R] P}
(h : Function.Injective ⇑g)
:
Function.Injective ⇑((IsLocalizedModule.map p f f') g)
theorem
surjective_localizationPreserves
{R : Type u_4}
[CommRing R]
(p : Submonoid R)
{M : Type u_6}
{N : Type u_7}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
{P : Type u_8}
{Q : Type u_9}
[AddCommGroup P]
[Module R P]
[AddCommGroup Q]
[Module R Q]
(f' : P →ₗ[R] Q)
[IsLocalizedModule p f']
{g : M →ₗ[R] P}
(h : Function.Surjective ⇑g)
:
Function.Surjective ⇑((IsLocalizedModule.map p f f') g)
theorem
bijective_localizationPreserves
{R : Type u_4}
[CommRing R]
(p : Submonoid R)
{M : Type u_6}
{N : Type u_7}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
[IsLocalizedModule p f]
{P : Type u_8}
{Q : Type u_9}
[AddCommGroup P]
[Module R P]
[AddCommGroup Q]
[Module R Q]
(f' : P →ₗ[R] Q)
[IsLocalizedModule p f']
{g : M →ₗ[R] P}
(h : Function.Bijective ⇑g)
:
Function.Bijective ⇑((IsLocalizedModule.map p f f') g)