case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(LinearMap.comp (↑(LinearEquiv.symm (iso S f))) f) m = ↑(LocalizedModule.mkLinearMap S M) m
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
⊢ LinearMap.comp (↑(LinearEquiv.symm (iso S f))) f = LocalizedModule.mkLinearMap S M
ext m
case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑↑(LinearEquiv.symm (iso S f)) (↑f m) = LocalizedModule.mk m 1
case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(LinearMap.comp (↑(LinearEquiv.symm (iso S f))) f) m = ↑(LocalizedModule.mkLinearMap S M) m
rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply]
case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(LinearEquiv.symm (iso S f)) (↑f m) = LocalizedModule.mk m 1
case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑↑(LinearEquiv.symm (iso S f)) (↑f m) = LocalizedModule.mk m 1
change (iso S f).symm _ = _
case h.eq1
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ 1 • ↑f m = ↑f m
case h
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(LinearEquiv.symm (iso S f)) (↑f m) = LocalizedModule.mk m 1
rw [iso_symm_apply']
no goals
case h.eq1
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.700210
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
m : M
⊢ 1 • ↑f m = ↑f m
exact one_smul _ _