theorem
injective_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M']
[Module R M']
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M →ₗ[R] M')
(h : ∀ (r : { x : R // x ∈ s }), Function.Injective ⇑((map' (Submonoid.powers ↑r)) f))
:
theorem
surjective_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M']
[Module R M']
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M →ₗ[R] M')
(h : ∀ (r : { x : R // x ∈ s }), Function.Surjective ⇑((map' (Submonoid.powers ↑r)) f))
:
theorem
bijective_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M']
[Module R M']
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M →ₗ[R] M')
(h : ∀ (r : { x : R // x ∈ s }), Function.Bijective ⇑((map' (Submonoid.powers ↑r)) f))
:
noncomputable def
linearEquivOfLocalizationFinitespan
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M']
[Module R M']
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M →ₗ[R] M')
(h : ∀ (r : { x : R // x ∈ s }), Function.Bijective ⇑((map' (Submonoid.powers ↑r)) f))
:
Equations
- linearEquivOfLocalizationFinitespan s spn f h = LinearEquiv.ofBijective f ⋯
Instances For
theorem
linearEquivOfLocalizationFinitespan_apply
{R : Type u_1}
{M : Type u_2}
{M' : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup M']
[Module R M']
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M →ₗ[R] M')
(h : ∀ (r : { x : R // x ∈ s }), Function.Bijective ⇑((map' (Submonoid.powers ↑r)) f))
(m : M)
:
(linearEquivOfLocalizationFinitespan s spn f h) m = f m