theorem Module.Flat.eqid (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ⋯.equiv = LinearEquiv.refl R (TensorProduct R (↥I) M)

theorem Module.Flat.diagram (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ⋯.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I) = ↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)

theorem Module.Flat.iff_isTensorProduct_lift_injective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ (I : Ideal R) {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] (f : ↥I →ₗ[R] M →ₗ[R] N) (h : IsTensorProduct f), Function.Injective ⇑(h.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

theorem Module.Flat.iff_exist_isTensorProduct_lift_injective (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ (I : Ideal R), ∃ (N : Type (max u v)) (x : AddCommGroup N) (x_1 : Module R N) (f : ↥I →ₗ[R] M →ₗ[R] N) (h : IsTensorProduct f), Function.Injective ⇑(h.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))

noncomputable def LinearMap.lTensor' {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) {N' : Type u_5} {P' : Type u_6} [AddCommMonoid N'] [AddCommMonoid P'] [Module R N'] [Module R P'] {fn : M →ₗ[R] N →ₗ[R] N'} (hn : IsTensorProduct fn) {fp : M →ₗ[R] P →ₗ[R] P'} (hp : IsTensorProduct fp) : N' →ₗ[R] P'

Equations

• f.lTensor' hn hp = hn.map hp LinearMap.id f

noncomputable def LinearMap.rTensor' {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) {N' : Type u_5} {P' : Type u_6} [AddCommMonoid N'] [AddCommMonoid P'] [Module R N'] [Module R P'] {fn : N →ₗ[R] M →ₗ[R] N'} (hn : IsTensorProduct fn) {fp : P →ₗ[R] M →ₗ[R] P'} (hp : IsTensorProduct fp) : N' →ₗ[R] P'

Equations

• f.rTensor' hn hp = hn.map hp f LinearMap.id

theorem Module.Flat.iff_exist_rTensor'_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → ∃ (P : Type v') (x : AddCommGroup P) (x_1 : Module R P) (p : N →ₗ[R] M →ₗ[R] P) (h : IsTensorProduct p) (P' : Type v') (x_2 : AddCommGroup P') (x_3 : Module R P') (p' : N' →ₗ[R] M →ₗ[R] P') (h' : IsTensorProduct p'), Function.Injective ⇑(f.rTensor' h h')

theorem Module.Flat.iff_exist_lTensor'_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → ∃ (P : Type v') (x : AddCommGroup P) (x_1 : Module R P) (p : M →ₗ[R] N →ₗ[R] P) (h : IsTensorProduct p) (P' : Type v') (x_2 : AddCommGroup P') (x_3 : Module R P') (p' : M →ₗ[R] N' →ₗ[R] P') (h' : IsTensorProduct p'), Function.Injective ⇑(f.lTensor' h h')

theorem Module.Flat.iff_exist_lTensor'_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, ∃ (P : Type v') (x : AddCommGroup P) (x_1 : Module R P) (p : M →ₗ[R] N →ₗ[R] P) (h : IsTensorProduct p) (P' : Type v') (x_2 : AddCommGroup P') (x_3 : Module R P') (p' : M →ₗ[R] N' →ₗ[R] P') (h' : IsTensorProduct p') (P'' : Type v') (x_4 : AddCommGroup P'') (x_5 : Module R P'') (p'' : M →ₗ[R] N'' →ₗ[R] P'') (h'' : IsTensorProduct p''), Function.Exact ⇑f ⇑g → Function.Exact ⇑(f.lTensor' h h') ⇑(g.lTensor' h' h'')

M is flat if and only if M ⊗ - is a left exact functor.

theorem Module.Flat.iff_exist_rTensor'_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, ∃ (P : Type v') (x : AddCommGroup P) (x_1 : Module R P) (p : N →ₗ[R] M →ₗ[R] P) (h : IsTensorProduct p) (P' : Type v') (x_2 : AddCommGroup P') (x_3 : Module R P') (p' : N' →ₗ[R] M →ₗ[R] P') (h' : IsTensorProduct p') (P'' : Type v') (x_4 : AddCommGroup P'') (x_5 : Module R P'') (p'' : N'' →ₗ[R] M →ₗ[R] P'') (h'' : IsTensorProduct p''), Function.Exact ⇑f ⇑g → Function.Exact ⇑(f.rTensor' h h') ⇑(g.rTensor' h' h'')

M is flat if and only if M ⊗ - is a left exact functor.

theorem Module.Flat.iff_rTensor'_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → ∀ {P : Type v'} [inst_4 : AddCommGroup P] [inst_5 : Module R P] {p : N →ₗ[R] M →ₗ[R] P} (h : IsTensorProduct p) {P' : Type v'} [inst_6 : AddCommGroup P'] [inst_7 : Module R P'] {p' : N' →ₗ[R] M →ₗ[R] P'} (h' : IsTensorProduct p'), Function.Injective ⇑(f.rTensor' h h')

theorem Module.Flat.iff_lTensor'_preserves_injective_linearMap (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → ∀ {P : Type v'} [inst_4 : AddCommGroup P] [inst_5 : Module R P] {p : M →ₗ[R] N →ₗ[R] P} (h : IsTensorProduct p) {P' : Type v'} [inst_6 : AddCommGroup P'] [inst_7 : Module R P'] {p' : M →ₗ[R] N' →ₗ[R] P'} (h' : IsTensorProduct p'), Function.Injective ⇑(f.lTensor' h h')

theorem Module.Flat.iff_lTensor'_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ {P : Type v'} [inst_6 : AddCommGroup P] [inst_7 : Module R P] {p : M →ₗ[R] N →ₗ[R] P} (h : IsTensorProduct p) {P' : Type v'} [inst_8 : AddCommGroup P'] [inst_9 : Module R P'] {p' : M →ₗ[R] N' →ₗ[R] P'} (h' : IsTensorProduct p') {P'' : Type v'} [inst_10 : AddCommGroup P''] [inst_11 : Module R P''] {p'' : M →ₗ[R] N'' →ₗ[R] P''} (h'' : IsTensorProduct p''), Function.Exact ⇑f ⇑g → Function.Exact ⇑(f.lTensor' h h') ⇑(g.lTensor' h' h'')

M is flat if and only if M ⊗ - is a left exact functor.

theorem Module.Flat.iff_rTensor'_exact (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] [Small.{v', u} R] [Small.{v', v} M] : Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ {P : Type v'} [inst_6 : AddCommGroup P] [inst_7 : Module R P] {p : N →ₗ[R] M →ₗ[R] P} (h : IsTensorProduct p) {P' : Type v'} [inst_8 : AddCommGroup P'] [inst_9 : Module R P'] {p' : N' →ₗ[R] M →ₗ[R] P'} (h' : IsTensorProduct p') {P'' : Type v'} [inst_10 : AddCommGroup P''] [inst_11 : Module R P''] {p'' : N'' →ₗ[R] M →ₗ[R] P''} (h'' : IsTensorProduct p''), Function.Exact ⇑f ⇑g → Function.Exact ⇑(f.rTensor' h h') ⇑(g.rTensor' h' h'')

M is flat if and only if M ⊗ - is a right exact functor.