theorem LocalizedModule.Localization.mk_cancel {R : Type u_1} [CommSemiring R] {S : Submonoid R} (r : R) (s : ↥S) (t : ↥S) : Localization.mk (r * ↑t) (s * t) = Localization.mk r s

theorem LocalizedModule.Localization.smul_mk_right_mul {R : Type u_1} [CommSemiring R] {S : Submonoid R} (r : R) (s : ↥S) (t : ↥S) : t • Localization.mk r (s * t) = Localization.mk r s

theorem LocalizedModule.mk_right_smul_mk {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommMonoid M] [Module R M] (m : M) (s : ↥S) (t : ↥S) : Localization.mk 1 s • LocalizedModule.mk m t = LocalizedModule.mk m (s * t)

theorem LocalizedModule.mk_right_smul_mk_left {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommMonoid M] [Module R M] (m : M) (s : ↥S) : Localization.mk 1 s • LocalizedModule.mk m 1 = LocalizedModule.mk m s

theorem LocalizedModule.mk_add_mk_right {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommMonoid M] [Module R M] (m : M) (n : M) (s : ↥S) : LocalizedModule.mk (m + n) s = LocalizedModule.mk m s + LocalizedModule.mk n s

theorem LocalizedModule.Localization.mk_eq_zero_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} (r : R) (s : ↥S) : Localization.mk r s = 0 ↔ ∃ (c : ↥S), ↑c * r = 0

theorem LocalizedModule.mk_eq_zero_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_3} [AddCommGroup M] [Module R M] (m : M) (s : ↥S) : LocalizedModule.mk m s = 0 ↔ ∃ (c : ↥S), c • m = 0

theorem LocalizedModule.wd_for_LiftOnLocalizationModule' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (a : M × ↥S) (b : M × ↥S) (h : LocalizedModule.r S M a b) : Localization.mk 1 a.2 • f a.1 = Localization.mk 1 b.2 • f b.1

def LocalizedModule.LiftOnLocalizationModule' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : LocalizedModule S M →ₗ[R] N

Equations

• One or more equations did not get rendered due to their size.

theorem LocalizedModule.LiftOnLocalizationModule'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (m : M) (s : ↥S) : (LocalizedModule.LiftOnLocalizationModule' S f) (LocalizedModule.mk m s) = Localization.mk 1 s • f m

theorem LocalizedModule.LiftOnLocalizationModule'_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : LocalizedModule.LiftOnLocalizationModule' S f ∘ₗ LocalizedModule.mkLinearMap S M = f

theorem LocalizedModule.LiftOnLocalizationModule'_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (g : LocalizedModule S M →ₗ[R] N) (h : g ∘ₗ LocalizedModule.mkLinearMap S M = f) : LocalizedModule.LiftOnLocalizationModule' S f = g

def LocalizedModule.LiftOnLocalizationModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : LocalizedModule S M →ₗ[Localization S] N

Equations

• LocalizedModule.LiftOnLocalizationModule S f = LinearMap.extendScalarsOfIsLocalization S (Localization S) (LocalizedModule.LiftOnLocalizationModule' S f)

theorem LocalizedModule.LiftOnLocalizationModule_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (m : M) (s : ↥S) : (LocalizedModule.LiftOnLocalizationModule S f) (LocalizedModule.mk m s) = Localization.mk 1 s • f m

theorem LocalizedModule.LiftOnLocalizationModule_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : ⇑(LocalizedModule.LiftOnLocalizationModule S f) ∘ ⇑(LocalizedModule.mkLinearMap S M) = ⇑f

theorem LocalizedModule.LiftOnLocalizationModule_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (g : LocalizedModule S M →ₗ[R] N) (h : g ∘ₗ LocalizedModule.mkLinearMap S M = f) : LocalizedModule.LiftOnLocalizationModule' S f = g

def LocalizedModule.lift.inv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {N : Type u_3} [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (s : ↥S) : Module.End R N

Equations

• LocalizedModule.lift.inv S s = { toFun := fun (n : N) => Localization.mk 1 s • n, map_add' := ⋯, map_smul' := ⋯ }

theorem LocalizedModule.lift.right_inv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {N : Type u_3} [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (s : ↥S) : (algebraMap R (Module.End R N)) ↑s * LocalizedModule.lift.inv S s = 1

theorem LocalizedModule.lift.left_inv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {N : Type u_3} [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (s : ↥S) : LocalizedModule.lift.inv S s * (algebraMap R (Module.End R N)) ↑s = 1

theorem LocalizedModule.lift.invertible {R : Type u_1} [CommSemiring R] (S : Submonoid R) {N : Type u_3} [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (s : ↥S) : IsUnit ((algebraMap R (Module.End R N)) ↑s)

theorem LocalizedModule.lift.isinv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {N : Type u_3} [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (s : ↥S) : ↑⋯.unit⁻¹ = LocalizedModule.lift.inv S s

noncomputable def LocalizedModule.lift.LiftOnLocalizationModule' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : LocalizedModule S M →ₗ[R] N

Equations

• LocalizedModule.lift.LiftOnLocalizationModule' S f = { toFun := ⇑(LocalizedModule.lift S f ⋯), map_add' := ⋯, map_smul' := ⋯ }

theorem LocalizedModule.lift.LiftOnLocalizationModule'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) (m : M) (s : ↥S) : (LocalizedModule.lift.LiftOnLocalizationModule' S f) (LocalizedModule.mk m s) = Localization.mk 1 s • f m

theorem LocalizedModule.LiftOnLocalization'_eq {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module (Localization S) N] [IsScalarTower R (Localization S) N] (f : M →ₗ[R] N) : LocalizedModule.LiftOnLocalizationModule' S f = LocalizedModule.lift.LiftOnLocalizationModule' S f

noncomputable def LocalizedModule.mapfromlift' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N

Equations

• LocalizedModule.mapfromlift' S = { toFun := fun (f : M →ₗ[R] N) => LocalizedModule.LiftOnLocalizationModule' S (LocalizedModule.mkLinearMap S N ∘ₗ f), map_add' := ⋯, map_smul' := ⋯ }

theorem LocalizedModule.mapfromlift'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (m : M) (s : ↥S) : ((LocalizedModule.mapfromlift' S) f) (LocalizedModule.mk m s) = LocalizedModule.mk (f m) s

noncomputable def LocalizedModule.mapfromlift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

Equations

• One or more equations did not get rendered due to their size.

theorem LocalizedModule.mapfromlift_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (m : M) (s : ↥S) : ((LocalizedModule.mapfromlift S) f) (LocalizedModule.mk m s) = LocalizedModule.mk (f m) s

noncomputable def LocalizedModule.LocalizedMapLift' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule S (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N

Equations

• LocalizedModule.LocalizedMapLift' S = LocalizedModule.LiftOnLocalizationModule' S (LocalizedModule.mapfromlift' S)

theorem LocalizedModule.LocalizedMapLift'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (m : M) (s : ↥S) (t : ↥S) : ((LocalizedModule.LocalizedMapLift' S) (LocalizedModule.mk f s)) (LocalizedModule.mk m t) = LocalizedModule.mk (f m) (s * t)

noncomputable def LocalizedModule.LocalizedMapLift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : LocalizedModule S (M →ₗ[R] N) →ₗ[Localization S] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

Equations

• LocalizedModule.LocalizedMapLift S = LocalizedModule.LiftOnLocalizationModule S (LocalizedModule.mapfromlift S)

theorem LocalizedModule.LocalizedMapLift_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (m : M) (s : ↥S) (t : ↥S) : ((LocalizedModule.LocalizedMapLift S) (LocalizedModule.mk f s)) (LocalizedModule.mk m t) = LocalizedModule.mk (f m) (s * t)

theorem LocalizedModule.Localization.r_iff_Localization_r {R : Type u_1} [CommSemiring R] (S : Submonoid R) (a : R × ↥S) (b : R × ↥S) : LocalizedModule.r S R a b ↔ (Localization.r S) a b

theorem LocalizedModule.Localization.mk_eq_iff_Localization_mk_eq {R : Type u_1} [CommSemiring R] (S : Submonoid R) (a : R × ↥S) (b : R × ↥S) : LocalizedModule.mk a.1 a.2 = LocalizedModule.mk b.1 b.2 ↔ Localization.mk a.1 a.2 = Localization.mk b.1 b.2

theorem LocalizedModule.Localization.r_tafe {R : Type u_1} [CommSemiring R] (S : Submonoid R) (a : R × ↥S) (b : R × ↥S) : [LocalizedModule.r S R a b, (Localization.r S) a b, (OreLocalization.oreEqv S R) a b, (Localization.r' S) a b].TFAE

theorem LocalizedModule.Localization.forliftOn {R : Type u_1} [CommSemiring R] (S : Submonoid R) {a : R} {c : R} {b : ↥S} {d : ↥S} (h : (Localization.r S) (a, b) (c, d)) : LocalizedModule.mk a b = LocalizedModule.mk c d

def LocalizedModule.Localization.Map {R : Type u_1} [CommSemiring R] (S : Submonoid R) : Localization S →ₐ[R] LocalizedModule S R

Equations

• LocalizedModule.Localization.Map S = { toFun := fun (x : Localization S) => x.liftOn LocalizedModule.mk ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem LocalizedModule.Localization.Map_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (r : R) (s : ↥S) : (LocalizedModule.Localization.Map S) (Localization.mk r s) = LocalizedModule.mk r s

theorem LocalizedModule.Localization.Map_surj {R : Type u_1} [CommSemiring R] (S : Submonoid R) : Function.Surjective ⇑(LocalizedModule.Localization.Map S)

theorem LocalizedModule.Localization.Map_inj {R : Type u_1} [CommSemiring R] (S : Submonoid R) : Function.Injective ⇑(LocalizedModule.Localization.Map S)

noncomputable def LocalizedModule.Localization.Equiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) : Localization S ≃ₐ[R] LocalizedModule S R

Equations

• LocalizedModule.Localization.Equiv S = AlgEquiv.ofBijective (LocalizedModule.Localization.Map S) ⋯

theorem LocalizedModule.Localization.Equiv_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (r : R) (s : ↥S) : (LocalizedModule.Localization.Equiv S) (Localization.mk r s) = LocalizedModule.mk r s

theorem LocalizedModule.Localization.Equiv_symm_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) (r : R) (s : ↥S) : (LocalizedModule.Localization.Equiv S).symm (LocalizedModule.mk r s) = Localization.mk r s