flat.lean

import category_theory.abelian.generator
import algebra.category.Module.monoidal
import algebra.module.injective
import ring_theory.flat

universe u

variables (R : Type u) [comm_ring R]

open category_theory.abelian category_theory opposite category_theory.monoidal_category
  category_theory.monoidal_closed

noncomputable theory

instance : enough_injectives (Module R) := sorry

lemma Module.is_generator_self : is_separator (Module.mk R : Module R) :=
begin
  rw is_separator_iff_faithful_coyoneda_obj,
  refine ⟨λ X Y f g e, _⟩,
  ext x,
  have := linear_map.congr_fun (congr_fun e (linear_map.to_span_singleton R X x) : _) (1 : R),
  dsimp at this,
  rwa one_smul at this,
end

lemma exists_cogenerator : ∃ M : Module.{u} R, injective M ∧ is_coseparator M :=
abelian.has_injective_coseparator _ (Module.is_generator_self R)

def cogenerator : Module.{u} R := (exists_cogenerator R).some

def cogenerator_is_injective : injective (cogenerator R) :=
  (exists_cogenerator R).some_spec.1

def cogenerator_is_coseparator : is_coseparator (cogenerator R) :=
  (exists_cogenerator R).some_spec.2

def dual : (Module.{u} R)ᵒᵖ ⥤ Module.{u} R := (linear_yoneda R _).obj (cogenerator R)

def internal_hom_forget : (linear_yoneda R $ Module.{u} R) ⋙ (whiskering_right _ _ _).obj (forget $ Module.{u} R) ≅ yoneda :=
iso.refl _

def dual_forget : dual R ⋙ forget _ ≅ yoneda.obj (cogenerator R) :=
(internal_hom_forget R).app _

instance : functor.preserves_monomorphisms (dual R) :=
begin
  haveI := functor.preserves_monomorphisms.of_iso (dual_forget R).symm,
  exact functor.preserves_monomorphisms_of_preserves_of_reflects (dual R) (forget _),
end

instance : functor.preserves_epimorphisms (dual R) :=
begin
  haveI : (yoneda.obj (cogenerator R)).preserves_epimorphisms,
  { rw ← injective.injective_iff_preserves_epimorphisms_yoneda_obj,
    exact cogenerator_is_injective R },
  haveI := functor.preserves_epimorphisms.of_iso (dual_forget R).symm,
  exact functor.preserves_epimorphisms_of_preserves_of_reflects (dual R) (forget _),
end

instance : faithful (dual R) :=
begin
  haveI : faithful (yoneda.obj (cogenerator R)),
  { rw [← is_coseparator_iff_faithful_yoneda_obj], exact cogenerator_is_coseparator _ },
  exact iso.faithful_of_comp (dual_forget R),
end

def hom_dual_iso_tensor_dual (M : Module.{u} R) :
  (linear_yoneda R $ Module.{u} R).obj ((dual R).obj $ op M) ≅ (tensor_right M).op ⋙ dual R :=
begin
  fapply nat_iso.of_components,
  { intro X,
    apply linear_equiv.to_Module_iso',
    exact tensor_product.lift.equiv R (unop X : _) M (cogenerator R) },
  { intros X Y f, ext1 g, dsimp, apply tensor_product.ext', intros x y,
    show tensor_product.uncurry R _ _ _ (f.unop ≫ g) (x ⊗ₜ[R] y) =
      tensor_product.uncurry R _ _ _ g (f.unop x ⊗ₜ[R] y),
    rw [tensor_product.uncurry_apply, tensor_product.uncurry_apply],
    refl },
end

lemma nat_iso.mono_iff {C D : Type*} [category C] [category D] {F G : C ⥤ D} (e : F ≅ G) {X Y : C}
  (f : X ⟶ Y) : mono (F.map f) ↔ mono (G.map f) :=
begin
  split,
  { rw ← nat_iso.naturality_2 e.symm f, introI _, apply_instance },
  { rw ← nat_iso.naturality_2 e f, introI _, apply_instance },
end

local attribute [instance] epi_comp

lemma nat_iso.epi_iff {C D : Type*} [category C] [category D] {F G : C ⥤ D} (e : F ≅ G) {X Y : C}
  (f : X ⟶ Y) : epi (F.map f) ↔ epi (G.map f) :=
begin
  split,
  { rw ← nat_iso.naturality_2 e.symm f, introI _, apply_instance },
  { rw ← nat_iso.naturality_2 e f, introI _, apply_instance },
end

lemma op_epi_iff_mono {C : Type*} [category C] {A B : C} (f : A ⟶ B) : epi f.op ↔ mono f :=
begin
  split, { introI, show mono f.op.unop, apply_instance }, { introI, apply_instance }
end

lemma epi_yoneda_dual_iff (M : Module.{u} R) {A B : Module.{u} R} (f : A ⟶ B) :
  epi ((yoneda.obj ((dual R).obj (op M))).map f.op) ↔
    mono ((tensor_right M).map f) :=
begin
  rw [← nat_iso.epi_iff ((internal_hom_forget R).app ((dual R).obj (op M))),
    ← op_epi_iff_mono, ← functor.epi_map_iff_epi (dual R)],
  show epi ((forget $ Module R).map _) ↔ _,
  rw functor.epi_map_iff_epi (forget $ Module R),
  exact nat_iso.epi_iff (hom_dual_iso_tensor_dual R M) f.op
end

lemma epi_yoneda_dual_iff' (M : Module.{u} R) {A B : (Module.{u} R)ᵒᵖ} (f : A ⟶ B) :
  epi ((yoneda.obj ((dual R).obj (op M))).map f) ↔
    mono ((tensor_right M).map f.unop) :=
epi_yoneda_dual_iff R M f.unop

open_locale tensor_product
open linear_map (lsmul)

universe v

@[mk_iff]
class module.flat' (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] : Prop :=
(out : ∀ ⦃I : ideal R⦄, function.injective (tensor_product.lift ((lsmul R M).comp I.subtype)))

attribute [mk_iff] functor.preserves_monomorphisms functor.preserves_epimorphisms

lemma functor.preserves_epimorphisms.comp_iff {C D E : Type*} [category C] [category D] [category E]
  (F : C ⥤ D) (G : D ⥤ E) [G.preserves_epimorphisms] [G.reflects_epimorphisms] :
    F.preserves_epimorphisms ↔ (F ⋙ G).preserves_epimorphisms :=
⟨λ _, by exactI infer_instance, λ _,
  by exactI functor.preserves_epimorphisms_of_preserves_of_reflects F G⟩

lemma functor.preserves_epimorphisms.op_iff {C D : Type*} [category C] [category D]
  (F : C ⥤ D) :
    F.op.preserves_epimorphisms ↔ F.preserves_monomorphisms :=
begin
  refine ⟨λ H, ⟨_⟩, λ H, ⟨_⟩⟩; introsI X Y f hf,
  { rw [← op_epi_iff_mono] at hf ⊢, exactI H.1 f.op },
  { show epi (F.map f.unop).op, haveI := H.1 f.unop, apply_instance },
end

lemma Module.injective_dual_iff (M : Module.{u} R) :
  injective ((dual R).obj $ op M) ↔
    functor.preserves_monomorphisms (tensor_right M) :=
begin
  rw [injective.injective_iff_preserves_epimorphisms_yoneda_obj,
    ← functor.preserves_epimorphisms.op_iff, category_theory.functor.preserves_epimorphisms_iff,
    category_theory.functor.preserves_epimorphisms_iff],
  simp_rw epi_yoneda_dual_iff',
  dsimp,
  simp_rw op_epi_iff_mono
end

lemma module.flat'_iff_mono (M : Module.{u} R) :
  module.flat' R M ↔ ∀ I : ideal R, mono
    ((tensor_right M).map $ Module.as_hom I.subtype) :=
begin
  rw module.flat'_iff,
  apply forall_congr,
  intro I,
  rw Module.mono_iff_injective,
  transitivity function.injective ((tensor_product.lid R M).symm.to_linear_map.comp
    (tensor_product.lift ((lsmul R ↥M).comp (submodule.subtype I)))),
  { exact ⟨λ H, (tensor_product.lid R M).symm.injective.comp H, λ H, H.of_comp⟩ },
  { congr' 3, apply tensor_product.ext', intros x y, dsimp, simpa only [tensor_product.tmul_smul,
      tensor_product.lift.tmul, algebra.id.smul_eq_mul, function.comp_app, linear_map.coe_comp,
      mul_one, linear_map.lsmul_apply, submodule.coe_subtype, tensor_product.smul_tmul'] }
end

lemma module.Baer_iff_surjective (M : Module.{u} R) :
  module.Baer.{u u} R M ↔ ∀ (I : ideal R), function.surjective
    ((yoneda.obj M).map (Module.as_hom (submodule.subtype I)).op) :=
begin
  split,
  { intros H I f, obtain ⟨g, hg⟩ := H I f, refine ⟨g, linear_map.ext $ λ ⟨x, h⟩, hg x h⟩ },
  { intros H I f, obtain ⟨g, rfl⟩ := H I f, exact ⟨g, λ _ _, rfl⟩ },
end

lemma module.Baer_iff_injective (M : Module.{u} R) :
  module.Baer.{u u} R M ↔ injective M :=
begin
  split,
  { intro H, have := module.Baer.injective.{u u} H,
    rw module.injective_iff_injective_object at this, cases M, exact this },
  { rw [module.Baer_iff_surjective, injective.injective_iff_preserves_epimorphisms_yoneda_obj],
    introsI H _,
    haveI : mono (Module.as_hom (submodule.subtype I)),
    { rw [Module.mono_iff_injective], exact submodule.injective_subtype I },
    rw ← epi_iff_surjective,
    apply H.1 },
end

lemma preserves_mono_iff (M : Module.{u} R) :
  module.flat' R M ↔ functor.preserves_monomorphisms (tensor_right M) :=
begin
  rw [module.flat'_iff_mono, ← Module.injective_dual_iff],
  simp_rw [← epi_yoneda_dual_iff, epi_iff_surjective],
  rw [← module.Baer_iff_surjective, module.Baer_iff_injective],
end