diff --git a/LeanCondensed.lean b/LeanCondensed.lean index de6e221..0ac6514 100644 --- a/LeanCondensed.lean +++ b/LeanCondensed.lean @@ -1,22 +1,14 @@ -import LeanCondensed.LightCondensed.Yoneda import LeanCondensed.Mathlib.CategoryTheory.Countable import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono -import LeanCondensed.Mathlib.CategoryTheory.Localization.Bifunctor -import LeanCondensed.Mathlib.CategoryTheory.Localization.Monoidal.Braided import LeanCondensed.Mathlib.CategoryTheory.Sites.DirectImage -import LeanCondensed.Mathlib.CategoryTheory.Sites.Monoidal import LeanCondensed.Mathlib.Condensed.Adjunctions import LeanCondensed.Mathlib.Condensed.Light.Limits import LeanCondensed.Mathlib.Condensed.Light.Monoidal -import LeanCondensed.Mathlib.Condensed.Light.Small -import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts import LeanCondensed.Projects.Epi import LeanCondensed.Projects.FreeCondensed -import LeanCondensed.Projects.InternallyProjective import LeanCondensed.Projects.IsLocalizedMonoidal import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.LightSolid -import LeanCondensed.Projects.LocalizedMonoidal import LeanCondensed.Projects.MonoidalLinear import LeanCondensed.Projects.PreservesCoprod import LeanCondensed.Projects.Proj diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean deleted file mode 100644 index f28d0d0..0000000 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ /dev/null @@ -1,94 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ - -import Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves -import Mathlib.CategoryTheory.Sites.Adjunction -import Mathlib.CategoryTheory.Sites.Canonical - -universe u - -noncomputable section - -open CategoryTheory Functor Sheaf GrothendieckTopology - -namespace Subcanonical - -variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J] - -variable (S S' : C) {A A' : (Sheaf J (Type _))} - -@[simps! apply] -def yoneda (A) : - (J.yoneda.obj S ⟶ A) ≃ A.val.obj ⟨S⟩ := - (fullyFaithfulSheafToPresheaf _ _).homEquiv.trans yonedaEquiv - -@[simp] -lemma yoneda_symm_apply_val_app (a : A.val.obj ⟨S⟩) (Y : Cᵒᵖ) (f : Y.unop ⟶ S) : - ((yoneda S A).symm a).val.app Y f = A.val.map f.op a := rfl - -lemma yoneda_symm_naturality {S' : C} (f : S' ⟶ S) - (x : A.val.obj ⟨S⟩) : J.yoneda.map f ≫ (yoneda S A).symm x = - (yoneda S' A).symm ((A.val.map f.op) x) := by - apply Sheaf.hom_ext - simp only [Sheaf.comp_val] - ext T y - simp only [FunctorToTypes.comp, yoneda_symm_apply_val_app, Opposite.op_unop] - rw [← FunctorToTypes.map_comp_apply (F := A.val)] - rfl - -attribute [local instance] Types.instConcreteCategory Types.instFunLike -lemma yoneda_symm_conaturality (f : A ⟶ A') - (x : A.val.obj ⟨S⟩) : (yoneda S A).symm x ≫ f = (yoneda S A').symm (f.val.app ⟨S⟩ x) := by - apply Sheaf.hom_ext - simp only [Sheaf.comp_val] - ext T y - exact NatTrans.naturality_apply (φ := f.val) (Y := T) _ _ - -lemma yoneda_conaturality (f : A ⟶ A') - (g : J.yoneda.obj S ⟶ A) - : f.val.app ⟨S⟩ (yoneda S A g) = yoneda S A' (g ≫ f) := rfl - -variable {D : Type*} [Category D] {FD : D → D → Type*} {DD : D → Type*} - [∀ X Y, FunLike (FD X Y) (DD X) (DD Y)] [ConcreteCategory D FD] - {free : Type _ ⥤ D} (adj : free ⊣ HasForget.forget) - [HasWeakSheafify J D] [J.HasSheafCompose (HasForget.forget (C := D))] - -variable (S S' : C) - -variable (A A' : (Sheaf J) D) - -abbrev forgetYoneda : - (J.yoneda.obj S ⟶ (sheafCompose J (HasForget.forget (C := D))).obj A) - ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) - := yoneda _ _ - -def freeYoneda : - ((J.yoneda ⋙ (composeAndSheafify J free)).obj S ⟶ A) ≃ (DD (A.val.obj ⟨S⟩)) - := ((adjunction _ adj).homEquiv _ _).trans (yoneda _ _) - -lemma freeYoneda_symm_naturality {S S'} (f : S' ⟶ S) - (x : DD (A.val.obj ⟨S⟩)) : (J.yoneda ⋙ composeAndSheafify J free).map f ≫ - (freeYoneda adj S A).symm x = (freeYoneda adj S' A).symm ((A.val.map f.op) x) := by - simp only [Functor.comp_obj, freeYoneda, Equiv.symm_trans_apply] - erw [Adjunction.homEquiv_counit, Adjunction.homEquiv_counit] - simp only [← Category.assoc] - erw [←Functor.map_comp (composeAndSheafify _ _), yoneda_symm_naturality] - rfl - -lemma freeYoneda_symm_conaturality (f : A ⟶ A') - (x : DD (A.val.obj ⟨S⟩)) : - (freeYoneda adj S A).symm x ≫ f = (freeYoneda adj S A').symm (f.val.app ⟨S⟩ x) := by - simp only [freeYoneda, Equiv.symm_trans_apply] - erw [←yoneda_symm_conaturality S - (A := (sheafCompose J (HasForget.forget (C := D))).obj A) - (f := (sheafCompose J (HasForget.forget (C := D))).map f) - ] - erw [Adjunction.homEquiv_counit, Adjunction.homEquiv_counit] - simp only [Category.assoc, Functor.comp_obj, Functor.map_comp] - erw [Adjunction.counit_naturality (adjunction J adj) f] - rfl - -end Subcanonical diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean deleted file mode 100644 index 7b53db1..0000000 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean +++ /dev/null @@ -1,34 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ -import Mathlib.CategoryTheory.Localization.Bifunctor - -namespace CategoryTheory - -open Category Functor - -variable {C₁ C₂ D₁ D₂ E E' : Type*} [Category C₁] [Category C₂] - [Category D₁] [Category D₂] [Category E] [Category E'] - -namespace Localization - -section - -variable (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂) - -variable (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) - (F : C₁ ⥤ C₂ ⥤ E) (F' : D₁ ⥤ D₂ ⥤ E) [Lifting₂ L₁ L₂ W₁ W₂ F F'] - -noncomputable instance Lifting₂.compRight {E' : Type*} [Category E'] [Lifting₂ L₁ L₂ W₁ W₂ F F'] - (G : E ⥤ E') : Lifting₂ L₁ L₂ W₁ W₂ - (F ⋙ (whiskeringRight _ _ _).obj G) - (F' ⋙ (whiskeringRight _ _ _).obj G) := - ⟨isoWhiskerRight (iso L₁ L₂ W₁ W₂ F F') ((whiskeringRight _ _ _).obj G)⟩ - -end - -end Localization - -end CategoryTheory diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean deleted file mode 100644 index a638761..0000000 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean +++ /dev/null @@ -1,253 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ -import Mathlib.CategoryTheory.Localization.Monoidal -import Mathlib.CategoryTheory.Monoidal.Braided.Basic - -/-! - -# Localization of symmetric monoidal categories - -Let `C` be a monoidal category equipped with a class of morphisms `W` which -is compatible with the monoidal category structure. The file -`Mathlib.CategoryTheory.Localization.Monoidal.Basic` constructs a monoidal structure on -the localized on `D` such that the localization functor is monoidal. - -In this file we promote this monoidal structure to a braided structure in the case where `C` is -braided, in such a way that the localization functor is braided. If `C` is symmetric monoidal, then -the monoidal structure on `D` is also symmetric. --/ - -open CategoryTheory Category MonoidalCategory BraidedCategory Functor - -namespace CategoryTheory.Localization.Monoidal - -variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) (W : MorphismProperty C) - [MonoidalCategory C] [W.IsMonoidal] [L.IsLocalization W] - {unit : D} (ε : L.obj (𝟙_ C) ≅ unit) - -local notation "L'" => toMonoidalCategory L W ε - -instance : (L').IsLocalization W := inferInstanceAs (L.IsLocalization W) - -lemma associator_hom (X Y Z : C) : (α_ ((L').obj X) ((L').obj Y) ((L').obj Z)).hom = - (Functor.LaxMonoidal.μ (L') X Y) ▷ (L').obj Z ≫ - (Functor.LaxMonoidal.μ (L') (X ⊗ Y) Z) ≫ - (L').map (α_ X Y Z).hom ≫ - (Functor.OplaxMonoidal.δ (L') X (Y ⊗ Z)) ≫ - ((L').obj X) ◁ (Functor.OplaxMonoidal.δ (L') Y Z) := by - simp - -lemma associator_inv (X Y Z : C) : (α_ ((L').obj X) ((L').obj Y) ((L').obj Z)).inv = - (L').obj X ◁ (Functor.LaxMonoidal.μ (L') Y Z) ≫ - (Functor.LaxMonoidal.μ (L') X (Y ⊗ Z)) ≫ - (L').map (α_ X Y Z).inv ≫ - (Functor.OplaxMonoidal.δ (L') (X ⊗ Y) Z) ≫ - (Functor.OplaxMonoidal.δ (L') X Y) ▷ ((L').obj Z) := by - simp - -section Braided - -variable [BraidedCategory C] - -noncomputable instance : Lifting₂ L' L' W W ((curriedTensor C) ⋙ (whiskeringRight C C - (LocalizedMonoidal L W ε)).obj L') (tensorBifunctor L W ε) := by - infer_instance - -noncomputable instance : Lifting₂ L' L' W W ((curriedTensor C).flip ⋙ (whiskeringRight C C - (LocalizedMonoidal L W ε)).obj L') (tensorBifunctor L W ε).flip := - inferInstanceAs (Lifting₂ L' L' W W (((curriedTensor C) ⋙ (whiskeringRight C C - (LocalizedMonoidal L W ε)).obj L')).flip (tensorBifunctor L W ε).flip ) - -/-- The braiding on the localized category as a natural isomorphism of bifunctors. -/ -noncomputable def braidingNatIso : tensorBifunctor L W ε ≅ (tensorBifunctor L W ε).flip := - lift₂NatIso L' L' W W - ((curriedTensor C) ⋙ (whiskeringRight C C - (LocalizedMonoidal L W ε)).obj L') - (((curriedTensor C).flip ⋙ (whiskeringRight C C - (LocalizedMonoidal L W ε)).obj L')) - _ _ (isoWhiskerRight (NatIso.ofComponents (fun X ↦ NatIso.ofComponents (fun Y ↦ β_ X Y))) _) - -lemma braidingNatIso_hom_app (X Y : C) : - ((braidingNatIso L W ε).hom.app ((L').obj X)).app ((L').obj Y) = - (Functor.LaxMonoidal.μ (L') X Y) ≫ - (L').map (β_ X Y).hom ≫ - (Functor.OplaxMonoidal.δ (L') Y X) := by - simp [braidingNatIso, lift₂NatIso] - rfl - -lemma braidingNatIso_hom_μ_left (X Y Z : C) : - ((braidingNatIso L W ε).hom.app ((L').obj X)).app ((L').obj Y ⊗ (L').obj Z) - ≫ (Functor.LaxMonoidal.μ (L') Y Z) ▷ (L').obj X = - (L').obj X ◁ (Functor.LaxMonoidal.μ (L') Y Z) ≫ - ((braidingNatIso L W ε).hom.app ((L').obj X)).app ((L').obj (Y ⊗ Z)) := by - erw [← ((braidingNatIso L W ε).hom.app ((L').obj X)).naturality - ((Functor.LaxMonoidal.μ (L') Y Z))] - rfl - -lemma braidingNatIso_hom_μ_right (X Y Z : C) : - ((braidingNatIso L W ε).hom.app ((L').obj X ⊗ (L').obj Y)).app ((L').obj Z) - ≫ (L').obj Z ◁ (Functor.LaxMonoidal.μ (L') X Y) = - (Functor.LaxMonoidal.μ (L') X Y) ▷ (L').obj Z ≫ - ((braidingNatIso L W ε).hom.app ((L').obj (X ⊗ Y))).app ((L').obj Z) := by - have := NatTrans.congr_app - ((braidingNatIso L W ε).hom.naturality ((Functor.LaxMonoidal.μ (L') X Y))) ((L').obj Z) - dsimp [Functor.flip] at this - erw [← this] - rfl - -@[reassoc] -lemma braiding_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : X' ⟶ Y') : - (f ⊗ₘ g) ≫ ((braidingNatIso L W ε).hom.app Y).app Y' = - ((braidingNatIso L W ε).hom.app X).app X' ≫ (g ⊗ₘ f) := by - rw [← id_comp f, ← comp_id g, tensor_comp, id_tensorHom, tensorHom_id, - tensor_comp, id_tensorHom, tensorHom_id, ← assoc] - erw [← ((braidingNatIso L W ε).app _).hom.naturality g] - simp only [assoc] - congr 1 - exact NatTrans.congr_app ((braidingNatIso L W ε).hom.naturality f) Y' - -lemma map_hexagon_forward (X Y Z : C) : - (α_ ((L').obj X) ((L').obj Y) ((L').obj Z)).hom ≫ - (((braidingNatIso L W ε).app ((L').obj X)).app (((L').obj Y) ⊗ ((L').obj Z))).hom ≫ - (α_ ((L').obj Y) ((L').obj Z) ((L').obj X)).hom = - (((braidingNatIso L W ε).app ((L').obj X)).app ((L').obj Y)).hom ▷ ((L').obj Z) ≫ - (α_ ((L').obj Y) ((L').obj X) ((L').obj Z)).hom ≫ - ((L').obj Y) ◁ (((braidingNatIso L W ε).app ((L').obj X)).app ((L').obj Z)).hom := by - simp only [associator_hom, Iso.app_hom, braidingNatIso_hom_app] - slice_rhs 0 4 => - simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, - Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, comp_whiskerRight, assoc, - Functor.Monoidal.whiskerRight_δ_μ_assoc, Functor.LaxMonoidal.μ_natural_left] - simp only [assoc] - congr 2 - slice_rhs 3 6 => - simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, MonoidalCategory.whiskerLeft_comp, - Functor.Monoidal.whiskerLeft_δ_μ_assoc, Functor.OplaxMonoidal.δ_natural_right_assoc] - simp only [← assoc] - slice_lhs 4 5 => - rw [braidingNatIso_hom_μ_left, braidingNatIso_hom_app] - simp - -lemma map_hexagon_reverse (X Y Z : C) : - (α_ ((L').obj X) ((L').obj Y) ((L').obj Z)).inv ≫ - (((braidingNatIso L W ε).app ((L').obj X ⊗ (L').obj Y)).app ((L').obj Z)).hom ≫ - (α_ ((L').obj Z) ((L').obj X) ((L').obj Y)).inv = - ((L').obj X) ◁ (((braidingNatIso L W ε).app ((L').obj Y)).app ((L').obj Z)).hom ≫ - (α_ ((L').obj X) ((L').obj Z) ((L').obj Y)).inv ≫ - (((braidingNatIso L W ε).app ((L').obj X)).app ((L').obj Z)).hom ▷ ((L').obj Y) := by - simp only [associator_inv, Iso.app_hom, braidingNatIso_hom_app] - slice_rhs 0 3 => - simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, - Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, assoc, - Functor.Monoidal.whiskerLeft_δ_μ, comp_id] - simp only [assoc] - congr 1 - slice_rhs 4 7 => - simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, comp_whiskerRight, - Functor.Monoidal.whiskerRight_δ_μ_assoc, Functor.OplaxMonoidal.δ_natural_left_assoc] - simp only [← assoc] - congr 2 - slice_rhs 0 3 => - simp only [Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, - Functor.LaxMonoidal.μ_natural_right_assoc] - simp only [assoc] - congr 1 - slice_lhs 4 5 => - rw [braidingNatIso_hom_μ_right, braidingNatIso_hom_app] - simp - -noncomputable instance : BraidedCategory (LocalizedMonoidal L W ε) where - braiding X Y := ((braidingNatIso L W ε).app X).app Y - braiding_naturality_right X Y Z f := ((braidingNatIso L W ε).app X).hom.naturality f - braiding_naturality_left {X Y} f Z := - NatTrans.congr_app ((braidingNatIso L W ε).hom.naturality f) Z - hexagon_forward X Y Z := by - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - obtain ⟨y, ⟨eY⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ - obtain ⟨z, ⟨eZ⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Z) := ⟨_, ⟨(L').objObjPreimageIso Z⟩⟩ - suffices (α_ ((L').obj x) ((L').obj y) ((L').obj z)).hom ≫ - (((braidingNatIso L W ε).app ((L').obj x)).app (((L').obj y) ⊗ ((L').obj z))).hom ≫ - (α_ ((L').obj y) ((L').obj z) ((L').obj x)).hom = - (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj y)).hom ▷ ((L').obj z) ≫ - (α_ ((L').obj y) ((L').obj x) ((L').obj z)).hom ≫ - ((L').obj y) ◁ (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj z)).hom by - refine Eq.trans ?_ ((((eX.inv ⊗ₘ eY.inv) ⊗ₘ eZ.inv) ≫= this =≫ - (eY.hom ⊗ₘ eZ.hom ⊗ₘ eX.hom)).trans ?_) - · simp only [Iso.app_hom, associator_conjugation, Functor.flip_obj_obj, assoc, - Iso.inv_hom_id_assoc, Iso.cancel_iso_hom_left] - rw [← Iso.eq_comp_inv] - simp [← associator_conjugation, ← braiding_naturality, ← whiskerLeft_comp_assoc] - · simp only [Functor.flip_obj_obj, Iso.app_hom, assoc, ← tensorHom_id] - simp only [← assoc] - rw [← tensor_comp, braiding_naturality] - simp only [Functor.flip_obj_obj, comp_id, assoc] - rw [← id_comp eZ.inv, tensor_comp, tensorHom_id] - rw [← id_tensorHom, ← tensor_comp, ← braiding_naturality] - simp [← whiskerLeft_comp_assoc] - exact map_hexagon_forward L W ε x y z - hexagon_reverse X Y Z := by - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - obtain ⟨y, ⟨eY⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ - obtain ⟨z, ⟨eZ⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Z) := ⟨_, ⟨(L').objObjPreimageIso Z⟩⟩ - suffices (α_ ((L').obj x) ((L').obj y) ((L').obj z)).inv ≫ - (((braidingNatIso L W ε).app ((L').obj x ⊗ (L').obj y)).app ((L').obj z)).hom ≫ - (α_ ((L').obj z) ((L').obj x) ((L').obj y)).inv = - ((L').obj x) ◁ (((braidingNatIso L W ε).app ((L').obj y)).app ((L').obj z)).hom ≫ - (α_ ((L').obj x) ((L').obj z) ((L').obj y)).inv ≫ - (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj z)).hom ▷ ((L').obj y) by - refine Eq.trans ?_ (((eX.inv ⊗ₘ (eY.inv ⊗ₘ eZ.inv)) ≫= this =≫ - ((eZ.hom ⊗ₘ eX.hom) ⊗ₘ eY.hom)).trans ?_) - · simp [← braiding_naturality_assoc, ← whiskerLeft_comp_assoc] - · simp only [Functor.flip_obj_obj, Iso.app_hom, assoc, ← id_tensorHom] - rw [← tensor_comp_assoc, braiding_naturality] - simp only [comp_id, Functor.flip_obj_obj, associator_conjugation, - MonoidalCategory.id_tensorHom] - rw [← id_comp eX.inv, tensor_comp, id_tensorHom] - simp only [← associator_conjugation] - rw [← tensorHom_id, ← tensor_comp, ← braiding_naturality] - simp only [Functor.flip_obj_obj, id_comp] - rw [← comp_id eY.hom, tensor_comp, tensorHom_id] - simp only [associator_conjugation, assoc, Iso.inv_hom_id_assoc, inv_hom_id_tensor_assoc, - MonoidalCategory.id_tensorHom] - rw [← whiskerLeft_comp_assoc, ← whiskerLeft_comp_assoc] - simp only [assoc, tensor_inv_hom_id, MonoidalCategory.tensorHom_id, inv_hom_whiskerRight, - MonoidalCategory.whiskerLeft_comp] - congr 1 - exact whiskerLeft_id_assoc X _ _ - exact map_hexagon_reverse L W ε x y z - -lemma β_hom_app (X Y : C) : - (β_ ((L').obj X) ((L').obj Y)).hom = - (Functor.LaxMonoidal.μ (L') X Y) ≫ - (L').map (β_ X Y).hom ≫ - (Functor.OplaxMonoidal.δ (L') Y X) := - braidingNatIso_hom_app L W ε X Y - -noncomputable instance : (toMonoidalCategory L W ε).Braided where - braided X Y := by simp [β_hom_app] - -end Braided - -section Symmetric - -variable [SymmetricCategory C] - -noncomputable instance : SymmetricCategory (LocalizedMonoidal L W ε) where - toBraidedCategory := inferInstance - symmetry X Y := by - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - obtain ⟨y, ⟨eY⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ - suffices (β_ ((L').obj x) ((L').obj y)).hom ≫ (β_ ((L').obj y) ((L').obj x)).hom = 𝟙 _ by - refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ - (eX.hom ⊗ₘ eY.hom)).trans ?_) - all_goals simp - simp [-Functor.map_braiding, β_hom_app, ← Functor.map_comp_assoc] - -end Symmetric - -end CategoryTheory.Localization.Monoidal diff --git a/LeanCondensed/Mathlib/CategoryTheory/Sites/Monoidal.lean b/LeanCondensed/Mathlib/CategoryTheory/Sites/Monoidal.lean deleted file mode 100644 index b277427..0000000 --- a/LeanCondensed/Mathlib/CategoryTheory/Sites/Monoidal.lean +++ /dev/null @@ -1,71 +0,0 @@ -/- -Copyright (c) 2024 Joël Riou. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joël Riou --/ - -import Mathlib.CategoryTheory.Sites.Monoidal -import LeanCondensed.Mathlib.CategoryTheory.Localization.Monoidal.Braided - -/-! -# Monoidal category structure on categories of sheaves - -If `A` is a closed braided category with suitable limits, -and `J` is a Grothendieck topology with `HasWeakSheafify J A`, -then `Sheaf J A` can be equipped with a monoidal category -structure. This is not made an instance as in some cases -it may conflict with monoidal structure deduced from -chosen finite products. - -## TODO - -* show that the monoidal category structure on sheaves is closed, -and that the internal hom can be defined in such a way that the -underlying presheaf is the internal hom in the category of presheaves. -Note that a `MonoidalClosed` instance on sheaves can already be obtained -abstractly using the material in `CategoryTheory.Monoidal.Braided.Reflection`. - --/ - -universe v v' u u' - -namespace CategoryTheory - -variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C} - {A : Type u} [Category.{v} A] [MonoidalCategory A] - -open Opposite Limits MonoidalCategory MonoidalClosed Enriched.FunctorCategory - -namespace Sheaf - -variable (J A) - -/-- The monoidal category structure on `Sheaf J A` obtained in `Sheaf.monoidalCategory` is -braided when `A` is braided. -/ -noncomputable def braidedCategory [(J.W (A := A)).IsMonoidal] [HasWeakSheafify J A] - [BraidedCategory A] : - letI := monoidalCategory J A - BraidedCategory (Sheaf J A) := - inferInstanceAs (BraidedCategory - (LocalizedMonoidal (L := presheafToSheaf J A) (W := J.W) (Iso.refl _))) - -/-- The monoidal category structure on `Sheaf J A` obtained in `Sheaf.monoidalCategory` is -symmetric when `A` is symmetric. -/ -noncomputable def symmetricCategory [(J.W (A := A)).IsMonoidal] [HasWeakSheafify J A] - [SymmetricCategory A] : - letI := monoidalCategory J A - SymmetricCategory (Sheaf J A) := - inferInstanceAs (SymmetricCategory - (LocalizedMonoidal (L := presheafToSheaf J A) (W := J.W) (Iso.refl _))) - -noncomputable instance [(J.W (A := A)).IsMonoidal] [HasWeakSheafify J A] - [BraidedCategory A] : - letI := monoidalCategory J A - letI := braidedCategory J A - (presheafToSheaf J A).Braided := - inferInstanceAs (Localization.Monoidal.toMonoidalCategory - (L := presheafToSheaf J A) (W := J.W) (Iso.refl _)).Braided - -end Sheaf - -end CategoryTheory diff --git a/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean b/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean index fbade41..8aa97d7 100644 --- a/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean +++ b/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean @@ -8,199 +8,21 @@ import Mathlib.CategoryTheory.Monoidal.Braided.Reflection import Mathlib.CategoryTheory.Monoidal.Braided.Transport import Mathlib.Condensed.Discrete.Module import Mathlib.Condensed.Light.CartesianClosed -import LeanCondensed.Mathlib.CategoryTheory.Sites.Monoidal -import LeanCondensed.Mathlib.Condensed.Light.Small -import LeanCondensed.Projects.SheafMonoidal +import Mathlib.Condensed.Light.Monoidal +import Mathlib.Condensed.Light.Small import LeanCondensed.Projects.MonoidalLinear universe u noncomputable section -open CategoryTheory Monoidal Sheaf MonoidalCategory MonoidalClosed MonoidalClosed.FunctorCategory - Functor - -section - -namespace CategoryTheory.MonoidalClosed -- TODO: move - -instance {C D : Type*} [Category C] [Category D] - (e : C ≌ D) [MonoidalCategory C] [MonoidalClosed C] : - MonoidalClosed (Transported e) := - MonoidalClosed.ofEquiv _ (equivalenceTransported e).symm.toAdjunction - -end CategoryTheory.MonoidalClosed - -variable {C D E : Type*} [Category C] [Category D] [Category E] - (e : C ≌ D) [MonoidalCategory C] [MonoidalCategory E] (F : Transported e ⥤ E) - (G : E ⥤ Transported e) - -def CategoryTheory.Equivalence.monoidalOfComp [(e.functor ⋙ F).Monoidal] : F.Monoidal := - monoidalTransport (e.invFunIdAssoc F) - -def CategoryTheory.Equivalence.monoidalOfComp' [(G ⋙ e.inverse).Monoidal] : G.Monoidal := - letI : (G ⋙ (equivalenceTransported e).inverse ⋙ (equivalenceTransported e).functor).Monoidal := - inferInstanceAs - ((G ⋙ (equivalenceTransported e).inverse) ⋙ (equivalenceTransported e).functor).Monoidal - monoidalTransport (isoWhiskerLeft G e.counitIso ≪≫ G.rightUnitor) - -end - -namespace CategoryTheory.Sheaf - -variable {C D : Type*} [Category C] [Category D] - {J : GrothendieckTopology C} - {A : Type*} [Category A] - {F G : D ⥤ Sheaf J A} (i : F ⋙ sheafToPresheaf _ _ ≅ G ⋙ sheafToPresheaf _ _) - -def natIsoCancel : F ≅ G := - NatIso.ofComponents (fun X ↦ (sheafToPresheaf _ _).preimageIso (i.app _)) (by - intro X Y f - apply (sheafToPresheaf _ _).map_injective - simpa [-sheafToPresheaf_map, -sheafToPresheaf_obj] using i.hom.naturality _) - -end CategoryTheory.Sheaf +open CategoryTheory namespace LightCondensed variable (R : Type u) [CommRing R] -attribute [local instance] monoidalCategory in -instance : MonoidalCategory (LightCondMod.{u} R) := - inferInstanceAs (MonoidalCategory (Transported (equivSmall (ModuleCat R)).symm)) - -instance : MonoidalCategory (Sheaf (coherentTopology LightProfinite.{u}) (ModuleCat.{u} R)) := - inferInstanceAs (MonoidalCategory (LightCondMod.{u} R)) - -attribute [local instance] monoidalCategory symmetricCategory in -instance : SymmetricCategory (LightCondMod.{u} R) := - inferInstanceAs (SymmetricCategory (Transported (equivSmall (ModuleCat R)).symm)) - -attribute [local instance] monoidalCategory in -def monoidalClosedSmallSheaves : MonoidalClosed - (Sheaf ((equivSmallModel.{u} LightProfinite.{u}).inverse.inducedTopology - (coherentTopology LightProfinite.{u})) (ModuleCat R)) := - Reflective.monoidalClosed (sheafificationAdjunction _ _) - -attribute [local instance] monoidalCategory monoidalClosedSmallSheaves in -instance : MonoidalClosed (LightCondMod.{u} R) := - inferInstanceAs (MonoidalClosed (Transported (equivSmall (ModuleCat R)).symm)) - --- Required to get sheafification. --- TODO: add a global instance for sheafification of type-valued sheaves -attribute [local instance] Types.instConcreteCategory - -attribute [local instance] monoidalCategory in -def monoidalOfPostcomp {E : Type*} [Category E] [MonoidalCategory E] (F : E ⥤ LightCondMod.{u} R) - [(F ⋙ (equivSmall _).functor).Monoidal] : F.Monoidal := - letI : (F ⋙ (equivSmall _).symm.inverse).Monoidal := - inferInstanceAs (F ⋙ (equivSmall _).functor).Monoidal - (equivSmall (ModuleCat R)).symm.monoidalOfComp' F - - -def monoidalOfPrecomp {E : Type*} [Category E] [MonoidalCategory E] (F : LightCondSet.{u} ⥤ E) - [((equivSmall _).inverse ⋙ F).Monoidal] : F.Monoidal := - letI : ((equivSmall _).symm.functor ⋙ F).Monoidal := - inferInstanceAs ((equivSmall _).inverse ⋙ F).Monoidal - letI : (equivSmall (Type u)).symm.inverse.Monoidal := - ((Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts - (equivSmall (Type u)).symm.inverse).mpr inferInstance).some - monoidalTransport ((equivSmall _).symm.invFunIdAssoc F) - -instance : (free R).Monoidal := by - letI : MonoidalCategory (Sheaf - ((equivSmallModel _).inverse.inducedTopology (coherentTopology LightProfinite.{u})) - (ModuleCat.{u} R)) := monoidalCategory _ _ - apply (config := {allowSynthFailures := true}) monoidalOfPostcomp - apply (config := {allowSynthFailures := true}) monoidalOfPrecomp - let i : (equivSmall (Type u)).inverse ⋙ free R ⋙ (equivSmall (ModuleCat R)).functor ≅ - Sheaf.composeAndSheafify _ (ModuleCat.free R) := by - refine natIsoCancel ?_ - let j := (((equivSmallModel LightProfinite.{u}).transportSheafificationAdjunction - (coherentTopology LightProfinite.{u}) - ((equivSmallModel _).inverse.inducedTopology (coherentTopology LightProfinite.{u})) - (ModuleCat.{u} R)).leftAdjointUniq - (sheafificationAdjunction (coherentTopology LightProfinite.{u}) _)).symm - calc _ ≅ ((equivSmall (Type u)).inverse ⋙ (sheafToPresheaf (coherentTopology LightProfinite.{u}) (Type u) ⋙ - (whiskeringRight LightProfinite.{u}ᵒᵖ (Type u) (ModuleCat.{u} R)).obj (ModuleCat.free R) ⋙ - (Equivalence.transportAndSheafify (coherentTopology LightProfinite) - ((equivSmallModel LightProfinite).inverse.inducedTopology (coherentTopology LightProfinite)) - (equivSmallModel LightProfinite) (ModuleCat R))) ⋙ - (equivSmall (ModuleCat.{u} R)).functor) ⋙ - sheafToPresheaf ((equivSmallModel LightProfinite.{u}).inverse.inducedTopology - (coherentTopology LightProfinite.{u})) (ModuleCat.{u} R) := ?_ - _ ≅ _ := ?_ - · exact isoWhiskerRight (isoWhiskerLeft _ (isoWhiskerRight (isoWhiskerLeft _ - (isoWhiskerLeft _ j)) _)) _ - · refine Functor.associator _ _ _ ≪≫ ?_ - refine isoWhiskerLeft _ (Functor.associator _ _ _) ≪≫ ?_ - refine isoWhiskerLeft _ (Functor.associator _ _ _) ≪≫ ?_ - refine isoWhiskerLeft _ (isoWhiskerLeft _ (Functor.associator _ _ _)) ≪≫ ?_ - refine isoWhiskerLeft _ (isoWhiskerLeft _ (isoWhiskerLeft _ (Functor.associator _ _ _))) ≪≫ ?_ - refine isoWhiskerLeft _ (isoWhiskerLeft _ (isoWhiskerLeft _ - (isoWhiskerLeft _ (Functor.associator _ _ _)))) ≪≫ ?_ - refine ?_ ≪≫ (Functor.associator _ _ _).symm - refine ?_ ≪≫ isoWhiskerLeft _ (Functor.associator _ _ _).symm - refine isoWhiskerLeft (equivSmall (Type u)).inverse - (isoWhiskerLeft (sheafToPresheaf (coherentTopology LightProfinite) (Type u)) (isoWhiskerLeft - ((whiskeringRight LightProfiniteᵒᵖ (Type u) (ModuleCat R)).obj (ModuleCat.free R)) - (isoWhiskerLeft (equivSmallModel LightProfinite).op.congrLeft.functor - (isoWhiskerLeft (H := sheafToPresheaf - ((equivSmallModel LightProfinite.{u}).inverse.inducedTopology - (coherentTopology LightProfinite.{u})) (ModuleCat.{u} R)) (presheafToSheaf - ((equivSmallModel LightProfinite.{u}).inverse.inducedTopology - (coherentTopology LightProfinite.{u})) - (ModuleCat.{u} R)) ?_)))) ≪≫ ?_ - · refine NatIso.ofComponents (fun X ↦ ?_) ?_ - · exact isoWhiskerRight (equivSmallModel LightProfinite.{u}).op.counitIso X.val ≪≫ - Functor.leftUnitor _ - · intros - ext - simp [Equivalence.sheafCongr, Equivalence.sheafCongr.functor, - Equivalence.sheafCongr.inverse] - · refine ?_ ≪≫ (Functor.associator _ _ _) - refine (Functor.associator _ _ _).symm ≪≫ ?_ - refine (Functor.associator _ _ _).symm ≪≫ ?_ - refine (Functor.associator _ _ _).symm ≪≫ ?_ - refine isoWhiskerRight ?_ _ - refine NatIso.ofComponents (fun X ↦ ?_) ?_ - · exact (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight - (isoWhiskerRight (equivSmallModel LightProfinite.{u}).op.counitIso X.val ≪≫ - Functor.leftUnitor _) (ModuleCat.free R) - · intros - apply NatTrans.ext - apply funext - intro - simp only [Equivalence.sheafCongr, Equivalence.sheafCongr.functor, - Equivalence.sheafCongr.inverse, Equivalence.congrLeft_functor, Equivalence.op_inverse, - Functor.comp_obj, sheafToPresheaf_obj, whiskeringRight_obj_obj, whiskeringLeft_obj_obj, - Functor.op_obj, Functor.comp_map, sheafToPresheaf_map, whiskeringRight_obj_map, - whiskeringLeft_obj_map, Equivalence.op_functor, Equivalence.op_counitIso, - isoWhiskerRight_trans, isoWhiskerRight_twice, Iso.trans_assoc, Iso.trans_hom, - Iso.symm_hom, isoWhiskerRight_hom, NatIso.op_inv, NatTrans.comp_app, - Functor.whiskerLeft_app, Functor.whiskerRight_app, - Functor.associator_inv_app, Functor.associator_hom_app, Functor.id_obj, NatTrans.op_app, - Functor.leftUnitor_hom_app, CategoryTheory.Functor.map_id, Category.comp_id, - Category.id_comp, Category.assoc] - simp [← Functor.map_comp] - exact monoidalTransport i.symm - -attribute [local instance] monoidalCategory in -instance : (equivSmall (ModuleCat R)).functor.Monoidal := - inferInstanceAs (equivalenceTransported (equivSmall (ModuleCat R)).symm).inverse.Monoidal - -attribute [local instance] monoidalCategory in -instance : (equivSmall (ModuleCat R)).inverse.Monoidal := by - exact (equivSmall (ModuleCat R)).inverseMonoidal - -instance : (equivSmall (ModuleCat R)).functor.Additive := - Functor.additive_of_preserves_binary_products _ - -instance : (equivSmall (ModuleCat R)).inverse.Additive := - Functor.additive_of_preserves_binary_products _ - -attribute [local instance] monoidalCategory CategoryTheory.Sheaf.monoidalPreadditive in -instance : MonoidalPreadditive (LightCondMod.{u} R) := by - apply monoidalPreadditive_of_faithful (equivSmall (ModuleCat R)).functor +instance : MonoidalPreadditive (LightCondMod.{u} R) := + CategoryTheory.Sheaf.monoidalPreadditive _ _ end LightCondensed diff --git a/LeanCondensed/Mathlib/Condensed/Light/Small.lean b/LeanCondensed/Mathlib/Condensed/Light/Small.lean deleted file mode 100644 index 33541c3..0000000 --- a/LeanCondensed/Mathlib/Condensed/Light/Small.lean +++ /dev/null @@ -1,40 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ -import Mathlib.CategoryTheory.Sites.Equivalence -import Mathlib.Condensed.Light.Basic - -/-! - -# Equivalence of light condensed objects with sheaves on a small site --/ - -universe u v w - -open CategoryTheory - -namespace LightCondensed - -variable {C : Type w} [Category.{v} C] - -variable (C) in -/-- -The equivalence of categories from light condensed objects to sheaves on a small site -equivalent to light profinite sets. --/ -noncomputable abbrev equivSmall : - LightCondensed.{u} C ≌ - Sheaf ((equivSmallModel.{u} LightProfinite.{u}).inverse.inducedTopology - (coherentTopology LightProfinite.{u})) C := - (equivSmallModel LightProfinite).sheafCongr _ _ _ - -instance (X Y : LightCondensed.{u} C) : Small.{max u v} (X ⟶ Y) where - equiv_small := - ⟨(equivSmall C).functor.obj X ⟶ (equivSmall C).functor.obj Y, - ⟨(equivSmall C).fullyFaithfulFunctor.homEquiv⟩⟩ - -instance : LocallySmall.{max u v} (LightCondensed.{u} C) where - -end LightCondensed diff --git a/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean b/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean deleted file mode 100644 index 649c085..0000000 --- a/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean +++ /dev/null @@ -1,97 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ -import Mathlib.Condensed.Light.CartesianClosed -import Mathlib.Condensed.Light.Functors -import Mathlib.Condensed.Light.TopCatAdjunction -import Mathlib.Topology.Compactness.PseudometrizableLindelof -import Mathlib.Topology.Connected.Separation -import Mathlib.Topology.EMetricSpace.Paracompact -import Mathlib.Topology.MetricSpace.Polish -import Mathlib.Topology.Separation.CompletelyRegular -import Mathlib.Topology.Spectral.Prespectral -import Mathlib.Topology.UniformSpace.DiscreteUniformity - -universe u - -open CategoryTheory Limits - -namespace CompHausLike - -variable {P : TopCat.{u} → Prop} (X Y : CompHausLike.{u} P) - (hP : HasProp P (X × Y)) - -def productCone : BinaryFan X Y := - BinaryFan.mk (P := CompHausLike.of P (X × Y)) - (TopCat.ofHom { toFun := Prod.fst }) (TopCat.ofHom { toFun := Prod.snd }) - -noncomputable def productIsLimit : IsLimit (productCone X Y hP) where - lift := fun S : BinaryFan X Y => TopCat.ofHom { - toFun := fun s => (S.fst s, S.snd s) - continuous_toFun := by continuity } - fac := by - rintro S (_ | _) <;> {dsimp; ext; rfl} - uniq := by - intro S m h - ext x - refine Prod.ext ?_ ?_ - · specialize h ⟨WalkingPair.left⟩ - apply_fun fun e => e x at h - exact h - · specialize h ⟨WalkingPair.right⟩ - apply_fun fun e => e x at h - exact h - -noncomputable def chosenFiniteProducts (hP : ∀ (X Y : CompHausLike.{u} P), HasProp P (X × Y)) - [HasProp P PUnit.{u + 1}] : CartesianMonoidalCategory (CompHausLike.{u} P) := - .ofChosenFiniteProducts - ⟨_, CompHausLike.isTerminalPUnit⟩ - (fun X Y ↦ ⟨productCone X Y (hP X Y), productIsLimit X Y (hP X Y)⟩) - -noncomputable instance : CartesianMonoidalCategory LightProfinite.{u} := - chosenFiniteProducts (fun _ _ => inferInstance) - -example : LightProfinite ⥤ TopCat := by exact LightProfinite.toTopCat - -instance {J : Type} [SmallCategory J] [CountableCategory J] : PreservesLimitsOfShape J - lightProfiniteToLightCondSet.{u} := by - have : Functor.IsRightAdjoint topCatToLightCondSet.{u} := - LightCondSet.topCatAdjunction.isRightAdjoint - haveI : PreservesLimitsOfShape J LightProfinite.toTopCat.{u} := - inferInstanceAs (PreservesLimitsOfShape J (lightToProfinite ⋙ Profinite.toTopCat)) - let i : lightProfiniteToLightCondSet.{u} ≅ - LightProfinite.toTopCat.{u} ⋙ topCatToLightCondSet.{u} := by - refine NatIso.ofComponents ?_ ?_ - · intro X - refine (sheafToPresheaf _ _).preimageIso ?_ - refine NatIso.ofComponents ?_ ?_ - intro S - · exact { - hom f := ⟨f.1, by continuity⟩ - inv f := TopCat.ofHom ⟨f.1, by continuity⟩ - hom_inv_id := rfl - inv_hom_id := rfl } - · aesop - · intro X Y f - apply (sheafToPresheaf _ _).map_injective - simp only [sheafToPresheaf_obj, Functor.comp_obj, topCatToSheafCompHausLike_obj, - TopCat.toSheafCompHausLike_val_obj, ContinuousMap.toFun_eq_coe, Functor.preimageIso_hom, - Functor.map_comp, Functor.map_preimage, Functor.comp_map, compHausLikeToTop_map] - ext S - simp [lightProfiniteToLightCondSet, topCatToLightCondSet] - rfl - exact preservesLimitsOfShape_of_natIso i.symm - --- TODO: add this general instance (preserves countable => preserves finite) -instance : PreservesFiniteLimits lightProfiniteToLightCondSet.{u} where - preservesFiniteLimits J := - haveI : CountableCategory J := inferInstance - inferInstance - -noncomputable instance : lightProfiniteToLightCondSet.Monoidal := by - have : Nonempty lightProfiniteToLightCondSet.Monoidal := by - rw [@Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts] - infer_instance - exact this.some diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index 22a615e..480bff3 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Jonas van der Schaaf. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jonas van der Schaaf -/ -import Mathlib.CategoryTheory.EffectiveEpi.RegularEpi +import Mathlib.CategoryTheory.Limits.Shapes.RegularMono import Mathlib.Combinatorics.Quiver.ReflQuiver import Mathlib.Condensed.Light.Epi import Mathlib.Condensed.Light.Explicit @@ -18,21 +18,6 @@ open Function CategoryTheory Limits Opposite universe u -namespace CategoryTheory.regularTopology - -theorem EqualizerCondition.bijective_mapToEqualizer_pullback' {C : Type*} [Category C] - (P : Cᵒᵖ ⥤ Type*) (hP : EqualizerCondition P) (X B : C) (π : X ⟶ B) [EffectiveEpi π] - (c : PullbackCone π π) (hc : IsLimit c) : - Function.Bijective (MapToEqualizer P π c.fst c.snd c.condition) := by - specialize hP π _ hc - rw [Types.type_equalizer_iff_unique] at hP - rw [Function.bijective_iff_existsUnique] - intro ⟨b, hb⟩ - obtain ⟨a, ha₁, ha₂⟩ := hP b hb - exact ⟨a, by simpa [MapToEqualizer] using ha₁, by simpa [MapToEqualizer] using ha₂⟩ - -end CategoryTheory.regularTopology - lemma surj_pullback' {X Y Z : LightProfinite.{u}} (f : X ⟶ Z) {g : Y ⟶ Z} (hf : Function.Surjective f) : Function.Surjective (CompHausLike.pullback.snd f g) := by intro y @@ -105,7 +90,7 @@ noncomputable def regularLiftElem {X Y : LightProfinite} (π : X ⟶ Y) [Effecti yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (CompHausLike.pullback.snd π π), ← this, ← this', cone.condition] LightCondensed.equalizerCondition cone.pt - |>.bijective_mapToEqualizer_pullback' _ _ _ π _ (CompHausLike.pullback.isLimit π π) + |>.bijective_mapToEqualizer_pullback' _ (CompHausLike.pullback.isLimit π π) |>.surjective ⟨fX, this⟩ |>.choose @@ -126,14 +111,14 @@ noncomputable def regularLift {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEp private lemma regularLift_prop {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) : - regularTopology.MapToEqualizer cone.pt.val π + regularTopology.mapToEqualizer cone.pt.val π (CompHausLike.pullback.fst π π) (CompHausLike.pullback.snd π π) (CompHausLike.pullback.condition _ _) (regularLiftElem π cone) = ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩ := LightCondensed.equalizerCondition cone.pt - |>.bijective_mapToEqualizer_pullback' _ _ _ π _ (CompHausLike.pullback.isLimit π π) + |>.bijective_mapToEqualizer_pullback' _ (CompHausLike.pullback.isLimit π π) |>.surjective ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩ |>.choose_spec @@ -160,14 +145,14 @@ noncomputable def explicitRegularIsColimit {X Y : LightProfinite} (π : X ⟶ Y) exact regular_IsColimit π noncomputable instance {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] : - RegularEpi (lightProfiniteToLightCondSet.map π) where + IsRegularEpi (lightProfiniteToLightCondSet.map π) := ⟨⟨{ W := lightProfiniteToLightCondSet.obj (CompHausLike.pullback π π) left := lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π) right := lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π) w := by rw [← lightProfiniteToLightCondSet.map_comp, ← lightProfiniteToLightCondSet.map_comp, CompHausLike.pullback.condition] - isColimit := regular_IsColimit π + isColimit := regular_IsColimit π }⟩⟩ instance : lightProfiniteToLightCondSet.PreservesEffectiveEpis where preserves _ _ := inferInstance diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean deleted file mode 100644 index ea165dd..0000000 --- a/LeanCondensed/Projects/InternallyProjective.lean +++ /dev/null @@ -1,301 +0,0 @@ -/- -Copyright (c) 2024 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson, Jonas van der Schaaf --/ -import Mathlib.Condensed.Light.Epi -import LeanCondensed.LightCondensed.Yoneda -import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono -import LeanCondensed.Mathlib.Condensed.Light.Limits -import LeanCondensed.Mathlib.Condensed.Light.Monoidal -import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts -/-! - -# Internal projectivity - -This file defines internal projectivity and provides explicit characterizations of -internal projectivity in the category of light condensed modules over a commutative ring. - --/ - -noncomputable section - -universe u - -open CategoryTheory MonoidalCategory Limits - -section InternallyProjective - -variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C] - -class InternallyProjective (P : C) : Prop where - preserves_epi : (ihom P).PreservesEpimorphisms - -theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X) : - InternallyProjective Y := - haveI : Retract (ihom Y) (ihom X) := { - i := MonoidalClosed.pre r.r - r := MonoidalClosed.pre r.i - retract := by - rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id] } - haveI _ := proj.preserves_epi - InternallyProjective.mk <| preservesEpi_ofRetract this - -end InternallyProjective - -open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory - MonoidalClosed Subcanonical Functor - -section Condensed - -attribute [local instance] Types.instConcreteCategory Types.instFunLike - -variable (R : Type u) [CommRing R] - -instance : (coherentTopology LightProfinite).HasSheafCompose (forget (ModuleCat.{u} R)) := - hasSheafCompose_of_preservesLimitsOfSize _ - -def ihomPoints (A B : LightCondMod.{u} R) (S : LightProfinite) : - ((ihom A).obj B).val.obj ⟨S⟩ ≃ ((A ⊗ ((free R).obj S.toCondensed)) ⟶ B) := - (freeYoneda (ModuleCat.adj.{u} R) _ _).symm.trans ((ihom.adjunction A).homEquiv _ _).symm --- We have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`, --- and this could be made an `≅`. But it's not needed in this proof. - - -lemma tensorLeft_obj (X Y : LightCondMod.{u} R) : (tensorLeft X).obj Y = X ⊗ Y := rfl - -lemma ihom_map_val_app (A B P : LightCondMod.{u} R) (S : LightProfinite) (e : A ⟶ B) : - ∀ x, ConcreteCategory.hom (((ihom P).map e).val.app ⟨S⟩) x = - (ihomPoints R P B S).symm (ihomPoints R P A S x ≫ e) := by - intro x - apply (ihomPoints R P B S).injective - simp only [ihomPoints, freeYoneda] - change ((((freeForgetAdjunction R).homEquiv S.toCondensed _).trans - (Subcanonical.yoneda S ((LightCondensed.forget R).obj _))).symm.trans - ((ihom.adjunction P).homEquiv _ _).symm) - ((ConcreteCategory.hom (((ihom P).map e).val.app (Opposite.op S))) x) = - ((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj B)).trans - (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj B)))).symm.trans - ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) B).symm) - (((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj B)).trans - (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj B)))).symm.trans - ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) B).symm).symm - (((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj A)).trans - (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj A)))).symm.trans - ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) A).symm) - x ≫ - e)) - simp only [curriedTensor_obj_obj, Equiv.trans_apply, - Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.symm_apply_apply] - erw [← Adjunction.homEquiv_naturality_right_symm] - erw [← Adjunction.homEquiv_naturality_right_symm] - simp only [Subcanonical.yoneda, sheafToPresheaf_obj, Equiv.symm_trans_apply, - curriedTensor_obj_obj, EmbeddingLike.apply_eq_iff_eq] - change (fullyFaithfulSheafToPresheaf _ _).homEquiv.symm _ = _ ≫ _ - apply (fullyFaithfulSheafToPresheaf _ _).map_injective - erw [Functor.FullyFaithful.homEquiv_symm_apply, Functor.FullyFaithful.homEquiv_symm_apply] - ext - simp [yonedaEquiv] - rfl - -lemma ihomPoints_symm_comp (B P : LightCondMod.{u} R) (S S' : LightProfinite) (π : S ⟶ S') - (f : _ ⟶ _) : - (ihomPoints R P B S).symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ f) = - ConcreteCategory.hom (((ihom P).obj B).val.map π.op) ((ihomPoints R P B S').symm f) := by - simp only [ihomPoints, Equiv.symm_trans_apply, Equiv.symm_symm] - simp only [freeYoneda, Subcanonical.yoneda, sheafToPresheaf_obj, Equiv.trans_apply] - change ((fullyFaithfulSheafToPresheaf _ _).homEquiv.trans _) - (((freeForgetAdjunction R).homEquiv _ _) - (((ihom.adjunction P).homEquiv _ _) _)) = _ - erw [Adjunction.homEquiv_apply, Adjunction.homEquiv_apply, Adjunction.homEquiv_apply, - Adjunction.homEquiv_apply] - simp only [Functor.comp_obj, ihom.ihom_adjunction_unit, Functor.map_comp] - simp only [← Functor.map_comp] - rw [(ihom P).map_comp, ← ihom.coev_naturality_assoc] - simp only [Functor.map_comp] - rw [Adjunction.unit_naturality_assoc] - erw [Equiv.trans_apply, Equiv.trans_apply, yonedaEquiv_comp, - Functor.FullyFaithful.homEquiv_apply, yonedaEquiv_comp] - simp only [comp_val, yonedaEquiv, yoneda_obj_obj, Opposite.op_unop, Equiv.coe_fn_mk, - FunctorToTypes.comp] - erw [← (((LightCondensed.forget R).map ((ihom P).map f)).val.naturality_apply π.op)] - simp only [ConcreteCategory.hom] - apply congrArg - simp only [← FunctorToTypes.comp] - erw [← ((LightCondensed.forget R).map ((ihom.coev P).app ((free R).obj - S'.toCondensed))).val.naturality_apply] - simp only [ConcreteCategory.hom, FunctorToTypes.comp] - apply congrArg - have : (lightProfiniteToLightCondSet.map π).val.app (Opposite.op S) (𝟙 S) = - S'.toCondensed.val.map π.op (𝟙 S') := rfl - rw [this] - simp - rfl - -def tensorFreeIso (X Y : LightCondSet.{u}) : - (free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⨯ Y) := - Functor.Monoidal.μIso (free R) X Y ≪≫ ((free R).mapIso - ((CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).conePointUniqueUpToIso - (limit.isLimit (pair X Y)))) - -def tensorFreeIso' (S T : LightProfinite) : - (free R).obj S.toCondensed ⊗ (free R).obj T.toCondensed ≅ - (free R).obj (S ⨯ T).toCondensed := tensorFreeIso R S.toCondensed T.toCondensed ≪≫ - (free R).mapIso (Limits.PreservesLimitPair.iso lightProfiniteToLightCondSet _ _).symm - -namespace LightCondensed - -lemma internallyProjective_iff_tensor_condition (P : LightCondMod R) : InternallyProjective P ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], - (∀ (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : P ⊗ (free R).obj S'.toCondensed ⟶ A), - (P ◁ ((lightProfiniteToLightCondSet ⋙ free R).map π)) ≫ g = g' ≫ e) := by - constructor - · intro ⟨h⟩ A B e he S g - have hh := h.1 e - rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite] at hh - specialize hh S ((ihomPoints R P B S).symm g) - obtain ⟨S', π, hπ, g', hh⟩ := hh - refine ⟨S', π, hπ, (ihomPoints _ _ _ _) g', ?_⟩ - rw [ihom_map_val_app] at hh - apply (ihomPoints R P B S').symm.injective - rw [hh] - exact ihomPoints_symm_comp R B P S' S π g - · intro h - constructor - constructor - intro A B e he - rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite] - intro S g - specialize h e S ((ihomPoints _ _ _ _) g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (ihomPoints _ _ _ _).symm g', ?_⟩ - rw [ihom_map_val_app] - have := ihomPoints_symm_comp R B P S' S π ((ihomPoints R P B S) g) - erw [hh] at this - simp [this] - rfl - -lemma internallyProjective_iff_tensor_condition' (P : LightCondMod R) : InternallyProjective P ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], - (∀ (S : LightProfinite) (g : (free R).obj S.toCondensed ⊗ P ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : (free R).obj S'.toCondensed ⊗ P ⟶ A), - (((lightProfiniteToLightCondSet ⋙ free R).map π) ▷ P) ≫ g = g' ≫ e) := by - rw [internallyProjective_iff_tensor_condition] - refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩ - · specialize h e S ((β_ _ _).hom ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (β_ _ _).inv ≫ g', ?_⟩ - simp [← hh] - · specialize h e S ((β_ _ _).inv ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (β_ _ _).hom ≫ g', ?_⟩ - simp [← hh] - -lemma free_internallyProjective_iff_tensor_condition (P : LightCondSet.{u}) : - InternallyProjective ((free R).obj P) ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], (∀ (S : LightProfinite) - (g : (free R).obj (P ⊗ S.toCondensed) ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : (free R).obj (P ⊗ S'.toCondensed) ⟶ A), - ((free R).map (P ◁ ((lightProfiniteToLightCondSet).map π))) ≫ g = g' ≫ e) := by - rw [internallyProjective_iff_tensor_condition] - refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩ - · specialize h e S ((Functor.Monoidal.μIso (free R) _ _).hom ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (Functor.Monoidal.μIso (free R) _ _).inv ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.comp_map, Functor.OplaxMonoidal.δ_natural_right, - Category.assoc, Functor.Monoidal.δ_μ, Category.comp_id] - · specialize h e S ((Functor.Monoidal.μIso (free R) _ _).inv ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (Functor.Monoidal.μIso (free R) _ _).hom ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.comp_map, ← Functor.LaxMonoidal.μ_natural_right, Category.assoc, - Functor.Monoidal.μ_δ, Category.comp_id] - -lemma free_internallyProjective_iff_tensor_condition' (P : LightCondSet.{u}) : - InternallyProjective ((free R).obj P) ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], (∀ (S : LightProfinite) - (g : (free R).obj (S.toCondensed ⊗ P) ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A), - ((free R).map (((lightProfiniteToLightCondSet).map π) ▷ P)) ≫ g = g' ≫ e) := by - rw [internallyProjective_iff_tensor_condition'] - refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩ - · specialize h e S ((Functor.Monoidal.μIso (free R) _ _).hom ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (Functor.Monoidal.μIso (free R) _ _).inv ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.comp_map, Functor.OplaxMonoidal.δ_natural_left, - Category.assoc, Functor.Monoidal.δ_μ, Category.comp_id] - · specialize h e S ((Functor.Monoidal.μIso (free R) _ _).inv ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (Functor.Monoidal.μIso (free R) _ _).hom ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.comp_map, ← Functor.LaxMonoidal.μ_natural_left, Category.assoc, - Functor.Monoidal.μ_δ, Category.comp_id] - -lemma free_lightProfinite_internallyProjective_iff_tensor_condition (P : LightProfinite.{u}) : - InternallyProjective ((free R).obj P.toCondensed) ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], (∀ (S : LightProfinite) - (g : (free R).obj ((P ⊗ S).toCondensed) ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : (free R).obj (P ⊗ S').toCondensed ⟶ A), - ((free R).map (lightProfiniteToLightCondSet.map (P ◁ π))) ≫ g = g' ≫ e) := by - rw [free_internallyProjective_iff_tensor_condition] - refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩ - · specialize h e S ((free R).map (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).hom ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (free R).map (Functor.Monoidal.μIso - lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [← Functor.map_comp, Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.OplaxMonoidal.δ_natural_right, - Category.assoc, Functor.Monoidal.δ_μ, Category.comp_id] - · specialize h e S ((free R).map (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).inv ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (free R).map - (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).hom ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [← Functor.map_comp, Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - ← Functor.LaxMonoidal.μ_natural_right, Category.assoc, - Functor.Monoidal.μ_δ, Category.comp_id] - -lemma free_lightProfinite_internallyProjective_iff_tensor_condition' (P : LightProfinite.{u}) : - InternallyProjective ((free R).obj P.toCondensed) ↔ - ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e], (∀ (S : LightProfinite) - (g : (free R).obj ((S ⊗ P).toCondensed) ⟶ B), ∃ (S' : LightProfinite) - (π : S' ⟶ S) (_ : Function.Surjective π) (g' : (free R).obj (S' ⊗ P).toCondensed ⟶ A), - ((free R).map (lightProfiniteToLightCondSet.map (π ▷ P))) ≫ g = g' ≫ e) := by - rw [free_internallyProjective_iff_tensor_condition'] - refine ⟨fun h A B e he S g ↦ ?_, fun h A B e he S g ↦ ?_⟩ - · specialize h e S ((free R).map (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).hom ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (free R).map (Functor.Monoidal.μIso - lightProfiniteToLightCondSet _ _).inv ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [← Functor.map_comp, Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - Functor.OplaxMonoidal.δ_natural_left, - Category.assoc, Functor.Monoidal.δ_μ, Category.comp_id] - · specialize h e S ((free R).map (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).inv ≫ g) - obtain ⟨S', π, hπ, g', hh⟩ := h - refine ⟨S', π, hπ, (free R).map - (Functor.Monoidal.μIso lightProfiniteToLightCondSet _ _).hom ≫ g', ?_⟩ - rw [Category.assoc, ← hh] - simp only [← Category.assoc] - simp only [← Functor.map_comp, Functor.Monoidal.μIso_hom, Functor.Monoidal.μIso_inv, - ← Functor.LaxMonoidal.μ_natural_left, Category.assoc, - Functor.Monoidal.μ_δ, Category.comp_id] - -end LightCondensed - -end Condensed diff --git a/LeanCondensed/Projects/IsLocalizedMonoidal.lean b/LeanCondensed/Projects/IsLocalizedMonoidal.lean index 6c9cb40..6a80250 100644 --- a/LeanCondensed/Projects/IsLocalizedMonoidal.lean +++ b/LeanCondensed/Projects/IsLocalizedMonoidal.lean @@ -3,7 +3,8 @@ Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dagur Asgeirsson -/ -import LeanCondensed.Projects.LocalizedMonoidal +import Mathlib.CategoryTheory.Localization.Monoidal.Functor +import Mathlib.CategoryTheory.Localization.Monoidal.Basic open CategoryTheory Localization.Monoidal MonoidalCategory @@ -28,8 +29,11 @@ def equivLocalizedMonoidal : D ≌ LocalizedMonoidal L W ε := CategoryTheory.Eq open Functor.Monoidal Functor.LaxMonoidal Functor.OplaxMonoidal instance [L.Monoidal] : (equivLocalizedMonoidal L W ε).inverse.Monoidal := - letI : (L ⋙ (equivLocalizedMonoidal L W ε).inverse).Monoidal := inferInstanceAs L.Monoidal - functorMonoidalOfComp L W ε _ + letI : (L' ⋙ (equivLocalizedMonoidal L W ε).inverse).Monoidal := inferInstanceAs L.Monoidal + letI : Localization.Lifting L W (L' ⋙ (equivLocalizedMonoidal L W ε).inverse) + (equivLocalizedMonoidal L W ε).inverse := ⟨Iso.refl _⟩ + functorMonoidalOfComp L' W (equivLocalizedMonoidal L W ε).inverse + (L' ⋙ (equivLocalizedMonoidal L W ε).inverse) instance [L.Monoidal] : (equivLocalizedMonoidal L W ε).functor.Monoidal := (equivLocalizedMonoidal L W ε).symm.inverseMonoidal diff --git a/LeanCondensed/Projects/LightProfiniteInjective.lean b/LeanCondensed/Projects/LightProfiniteInjective.lean index 38fba8d..10e109d 100644 --- a/LeanCondensed/Projects/LightProfiniteInjective.lean +++ b/LeanCondensed/Projects/LightProfiniteInjective.lean @@ -34,134 +34,121 @@ along a presentation of S as sequential limit of finite spaces. The key lemma is * -/ - noncomputable section universe u open Set Profinite Topology CategoryTheory LightProfinite Fin Limits -/- - For every closed Z ⊆ open U ⊆ profinite X, there is a clopen C with - Z ⊆ C ⊆ U. Perhaps this should go in mathlib somewhere? --/ - namespace Profinite -lemma clopen_of_closed_subset_open (X : Profinite.{u}) (Z U : Set X) - (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : +/-- In a totally disconnected compact Hausdorff space `X`, if `Z ⊆ U` are subsets with `Z` closed +and `U` open, there exists a clopen `C` with `Z ⊆ C ⊆ U`. -/ +lemma exists_clopen_of_closed_subset_open {X : Type u} + [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] + {Z U : Set X} (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : ∃ C : Set X, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U := by - -- every z ∈ Z has clopen neighborhood V z ⊆ U + -- every `z ∈ Z` has clopen neighborhood `V z ⊆ U` choose V hV using fun (z : Z) ↦ compact_exists_isClopen_in_isOpen hU (hZU z.property) - -- the V z cover Z + -- the `V z` cover `Z` have V_cover : Z ⊆ iUnion V := fun z hz ↦ mem_iUnion.mpr ⟨⟨z, hz⟩, (hV ⟨z, hz⟩).2.1⟩ - -- there is a finite subcover - choose I hI using IsCompact.elim_finite_subcover (IsClosed.isCompact hZ) - V (fun z ↦ (hV z).1.2) V_cover - -- the union C of this finite subcover does the job - let C := ⋃ (i ∈ I), V i - have C_clopen : IsClopen C := Finite.isClopen_biUnion (Finset.finite_toSet I) - (fun i _ ↦ (hV i).1) - have C_subset_U : C ⊆ U := by simp_all only [iUnion_subset_iff, C, implies_true] - exact ⟨C, C_clopen, hI, C_subset_U⟩ + -- choose a finite subcover + choose I hI using hZ.isCompact.elim_finite_subcover V (fun z ↦ (hV z).1.isOpen) V_cover + -- the union of this finite subcover does the job + exact ⟨⋃ (i ∈ I), V i, I.finite_toSet.isClopen_biUnion (fun i _ ↦ (hV i).1), hI, by simp_all⟩ /- Let X be profinite, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. - Assume that all the Z i are disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i + Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i with the C i disjoint, and such that ∪ C i = ∪ D i -/ lemma clopen_partition_of_disjoint_closeds_in_clopens - (X : Profinite.{u}) (n : ℕ) (Z : Fin n → Set X) (D : Fin n → Set X) + {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] + {I : Type*} [Finite I] {Z D : I → Set X} (Z_closed : ∀ i, IsClosed (Z i)) (D_clopen : ∀ i, IsClopen (D i)) - (Z_subset_D : ∀ i, Z i ⊆ D i) (Z_disj : ∀ i j, i < j → Disjoint (Z i) (Z j) ) : - ∃ C : Fin n → Set X, (∀ i, IsClopen (C i)) ∧ (∀ i, Z i ⊆ C i) ∧ (∀ i, C i ⊆ D i) ∧ - (⋃ i, D i) ⊆ (⋃ i, C i) ∧ (∀ i j, i < j → Disjoint (C i) (C j)) := by - induction n - case zero => - -- single Z given, can take C 0 = D - use fun _ ↦ univ -- empty range, can use junk - exact ⟨elim0, fun i ↦ elim0 i, fun i ↦ elim0 i, by - simp only [iUnion_of_empty]; trivial, fun i j ↦ elim0 i⟩ - case succ n ih => + (Z_subset_D : ∀ i, Z i ⊆ D i) (Z_disj : univ.PairwiseDisjoint Z) : + ∃ C : I → Set X, (∀ i, IsClopen (C i)) ∧ (∀ i, Z i ⊆ C i) ∧ (∀ i, C i ⊆ D i) ∧ + (⋃ i, D i) ⊆ (⋃ i, C i) ∧ (univ.PairwiseDisjoint C) := by + induction I using Finite.induction_empty_option with + | of_equiv e IH => + obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e) + (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i)) + (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image]) + refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i), + fun i ↦ by simpa using h3 (e.symm i), ?_, + by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩ + simp only [Function.comp_apply, iUnion_subset_iff] at h4 ⊢ + intro i + simpa [e.symm.surjective.iUnion_comp C] using h4 (e.symm i) + | h_empty => exact ⟨fun _ ↦ univ, by simp, by simp, by simp, by simp, fun i ↦ PEmpty.elim i⟩ + | @h_option I _ IH => -- let Z' be the restriction of Z along succ : Fin n → Fin (n+1) - let Z' : Fin n → Set X := fun i ↦ Z (succ i) - have Z'_closed (i : Fin n) : IsClosed (Z' i) := Z_closed (succ i) - have Z'_disj (i j : Fin n) (hij : i < j) : Disjoint (Z' i) (Z' j) := - Z_disj (succ i) (succ j) (succ_lt_succ_iff.mpr hij) + let Z' : I → Set X := fun i ↦ Z (some i) + have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i) + have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by + rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image] + exact PairwiseDisjoint.subset Z_disj (by simp) -- find Z 0 ⊆ V ⊆ D 0 \ ⋃ Z' using clopen_sandwich - let U : Set X := D 0 \ iUnion Z' - have U_open : IsOpen U := IsOpen.sdiff (D_clopen 0).2 - (isClosed_iUnion_of_finite Z'_closed) - have Z0_subset_U : Z 0 ⊆ U := subset_diff.mpr ⟨Z_subset_D 0, - disjoint_iUnion_right.mpr (fun i ↦ Z_disj 0 (succ i) (succ_pos ↑↑i))⟩ + let U : Set X := D none \ iUnion (Z ∘ some) + have U_open : IsOpen U := IsOpen.sdiff (D_clopen none).2 + (isClosed_iUnion_of_finite (fun i ↦ Z_closed (some i))) + have Z0_subset_U : Z none ⊆ U := by + rw [subset_diff] + simpa using ⟨Z_subset_D none, fun i ↦ (by apply Z_disj; all_goals simp)⟩ obtain ⟨V, V_clopen, Z0_subset_V, V_subset_U⟩ := - clopen_of_closed_subset_open X (Z 0) U (Z_closed 0) U_open Z0_subset_U - have V_subset_D0 : V ⊆ D 0 := subset_trans V_subset_U diff_subset + exists_clopen_of_closed_subset_open (Z_closed none) U_open Z0_subset_U + have V_subset_D0 : V ⊆ D none := subset_trans V_subset_U diff_subset -- choose Z' i ⊆ C' i ⊆ D' i = D i.succ \ V using induction hypothesis - let D' : Fin n → Set X := fun i ↦ D (succ i) \ V - have D'_clopen (i : Fin n): IsClopen (D' i) := IsClopen.diff (D_clopen i.succ) V_clopen - have Z'_subset_D' (i : Fin n) : Z' i ⊆ D' i := by - apply subset_diff.mpr - constructor - · exact Z_subset_D (succ i) - · apply Disjoint.mono_right V_subset_U - exact Disjoint.mono_left (subset_iUnion_of_subset i fun ⦃_⦄ h ↦ h) disjoint_sdiff_right + let D' : I → Set X := fun i ↦ D (some i) \ V + have D'_clopen (i : I): IsClopen (D' i) := IsClopen.diff (D_clopen (some i)) V_clopen + have Z'_subset_D' (i : I) : Z' i ⊆ D' i := by + rw [subset_diff] + refine ⟨by grind, Disjoint.mono_right V_subset_U ?_⟩ + exact Disjoint.mono_left (subset_iUnion_of_subset i fun _ h ↦ h) disjoint_sdiff_right obtain ⟨C', C'_clopen, Z'_subset_C', C'_subset_D', C'_cover_D', C'_disj⟩ := - ih Z' D' Z'_closed D'_clopen Z'_subset_D' Z'_disj - have C'_subset_D (i : Fin n): C' i ⊆ D (succ i) := subset_trans (C'_subset_D' i) diff_subset + IH Z'_closed D'_clopen Z'_subset_D' Z'_disj + have C'_subset_D (i : I): C' i ⊆ D (some i) := subset_trans (C'_subset_D' i) diff_subset -- now choose C0 = D 0 \ ⋃ C' i - let C0 : Set X := D 0 \ iUnion (fun i ↦ C' i) - have C0_subset_D0 : C0 ⊆ D 0 := diff_subset - have C0_clopen : IsClopen C0 := IsClopen.diff (D_clopen 0) (isClopen_iUnion_of_finite C'_clopen) - have Z0_subset_C0 : Z 0 ⊆ C0 := by + let C0 : Set X := D none \ iUnion (fun i ↦ C' i) + have C0_subset_D0 : C0 ⊆ D none := diff_subset + have C0_clopen : IsClopen C0 := IsClopen.diff (D_clopen none) + (isClopen_iUnion_of_finite C'_clopen) + have Z0_subset_C0 : Z none ⊆ C0 := by unfold C0 apply subset_diff.mpr constructor - · exact Z_subset_D 0 + · exact Z_subset_D none · apply Disjoint.mono_left Z0_subset_V - exact disjoint_iUnion_right.mpr fun i ↦ Disjoint.mono_right (C'_subset_D' i) disjoint_sdiff_right + exact disjoint_iUnion_right.mpr fun i ↦ Disjoint.mono_right (C'_subset_D' i) + disjoint_sdiff_right -- patch together to define C := cases C0 C', and verify the needed properties - let C : Fin (n+1) → Set X := cases C0 C' - have C_clopen : ∀ i, IsClopen (C i) := cases C0_clopen C'_clopen - have Z_subset_C : ∀ i, Z i ⊆ C i := cases Z0_subset_C0 Z'_subset_C' - have C_subset_D : ∀ i, C i ⊆ D i := cases C0_subset_D0 C'_subset_D - have C_cover_D : (⋃ i, D i) ⊆ (⋃ i, C i) := by -- messy, but I don't see easy simplification + let C : Option I → Set X := fun i ↦ Option.casesOn i C0 C' + have C_clopen : ∀ i, IsClopen (C i) := fun i ↦ Option.casesOn i C0_clopen C'_clopen + have Z_subset_C : ∀ i, Z i ⊆ C i := fun i ↦ Option.casesOn i Z0_subset_C0 Z'_subset_C' + have C_subset_D : ∀ i, C i ⊆ D i := fun i ↦ Option.casesOn i C0_subset_D0 C'_subset_D + have C_cover_D : (⋃ i, D i) ⊆ (⋃ i, C i) := by intro x hx - rw [mem_iUnion] - by_cases hx0 : x ∈ C0 - · exact ⟨0, hx0⟩ - · by_cases hxD : x ∈ D 0 - · have hxC' : x ∈ iUnion C' := by - rw [mem_diff] at hx0 - push_neg at hx0 - exact hx0 hxD - obtain ⟨i, hi⟩ := mem_iUnion.mp hxC' - exact ⟨i.succ, hi⟩ - · obtain ⟨i, hi⟩ := mem_iUnion.mp hx - have hi' : i ≠ 0 := by - intro h - rw [h] at hi - tauto - let j := i.pred hi' - have hij : i = j.succ := (pred_eq_iff_eq_succ hi').mp rfl - rw [hij] at hi - have hxD' : x ∈ ⋃ i, D' i := by - apply mem_iUnion.mpr ⟨j, _⟩ - apply mem_diff_of_mem hi - exact fun h ↦ hxD (V_subset_D0 h) - apply C'_cover_D' at hxD' - obtain ⟨k, hk⟩ := mem_iUnion.mp hxD' - exact ⟨k.succ, hk⟩ - have C_disj (i j : Fin (n+1)) (hij : i < j) : Disjoint (C i) (C j) := by - by_cases hi : i = 0 - · rw [hi]; rw [hi] at hij - rw [(pred_eq_iff_eq_succ (Fin.pos_iff_ne_zero.mp hij)).mp rfl] -- j = succ _ - apply Disjoint.mono_right (subset_iUnion (fun i ↦ C' i) (j.pred (ne_zero_of_lt hij))) - exact disjoint_sdiff_left - · have hj : j ≠ 0 := ne_zero_of_lt hij - rw [(pred_eq_iff_eq_succ hi).mp rfl, (pred_eq_iff_eq_succ hj).mp rfl] - exact C'_disj (i.pred hi) (j.pred hj) (pred_lt_pred_iff.mpr hij) + rw [mem_iUnion] at hx ⊢ + by_cases hx0 : x ∈ C0; { exact ⟨none, hx0⟩ } + by_cases hxD : x ∈ D none + · have hxC' : x ∈ ⋃ i, C' i := by grind + obtain ⟨i, hi⟩ := mem_iUnion.mp hxC' + exact ⟨some i, hi⟩ + · obtain ⟨none | j, hi⟩ := hx; {grind} + have hxD' : x ∈ ⋃ i, D' i := mem_iUnion.mpr ⟨j, by grind⟩ + obtain ⟨k, hk⟩ := mem_iUnion.mp <| C'_cover_D' hxD' + exact ⟨some k, hk⟩ + have C_disj : univ.PairwiseDisjoint C := by + rw [Set.pairwiseDisjoint_iff] + rintro (none | i) _ (none | j) _ + · simp + · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using + Disjoint.mono_right (subset_iUnion (fun i ↦ C' i) j) disjoint_sdiff_left + · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using + Disjoint.mono_left (subset_iUnion (fun j ↦ C' j) i) disjoint_sdiff_right + · simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) + (i := i) (by trivial) (j := j) (by trivial) exact ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ @@ -179,103 +166,68 @@ lemma clopen_partition_of_disjoint_closeds_in_clopens take Z s to be the fiber of g at s, and D s the fiber of g' at f' s -/ -lemma key_extension_lemma (X Y S T : Profinite.{u}) [Finite S] - (f : X → Y) (hf : Continuous f) (f_inj : Function.Injective f) - (f' : S → T) (f'_surj : Function.Surjective f') - (g : X → S) (hg : Continuous g) (g' : Y → T) (hg' : Continuous g') - (h_comm : g' ∘ f = f' ∘ g) : +lemma key_extension_lemma (X Y S T : Type u) + [TopologicalSpace X] [CompactSpace X] + [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] + [TopologicalSpace S] [T2Space S] [Finite S] + [TopologicalSpace T] [T2Space T] + (f : X → Y) (hf : Continuous f) (f_inj : Function.Injective f) + (f' : S → T) (f'_surj : Function.Surjective f') + (g : X → S) (hg : Continuous g) (g' : Y → T) (hg' : Continuous g') + (h_comm : g' ∘ f = f' ∘ g) : ∃ k : Y → S, (Continuous k) ∧ (f' ∘ k = g') ∧ (k ∘ f = g) := by - -- help the instance inference a bit: T is finite - letI : Finite T := Finite.of_surjective f' f'_surj + have : Finite T := Finite.of_surjective f' f'_surj -- pick bijection between Fin n and S - obtain ⟨n, φ, ψ, h1, h2⟩ := Finite.exists_equiv_fin S + -- obtain ⟨n, φ, ψ, h1, h2⟩ := Finite.exists_equiv_fin S -- define Z i to be the image of the fiber of g at i - let Z : Fin n → Set Y := fun i ↦ f '' (g⁻¹' {ψ i}) + let Z : S → Set Y := fun i ↦ f '' (g⁻¹' {i}) have Z_closed (i) : IsClosed (Z i) := (IsClosedEmbedding.isClosed_iff_image_isClosed (Continuous.isClosedEmbedding hf f_inj)).mp (IsClosed.preimage hg isClosed_singleton) - have Z_disj (i j) (hij : i < j) : Disjoint (Z i) (Z j) := by - apply (disjoint_image_iff f_inj).mpr - apply Disjoint.preimage g - apply disjoint_singleton.mpr - exact Function.Injective.ne (Function.LeftInverse.injective h2) (Fin.ne_of_lt hij) + have Z_disj : univ.PairwiseDisjoint Z := by + rw [Set.pairwiseDisjoint_iff] + simp only [image_inter_nonempty_iff, Z] + rintro _ _ _ _ ⟨_, rfl, ⟨_, rfl, hy⟩⟩ + rw [f_inj hy] -- define D i to be the fiber of g' at f' i - let D : Fin n → Set Y := fun i ↦ g' ⁻¹' ( {f' (ψ i)}) - have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' (ψ i)}) hg' + let D : S → Set Y := fun i ↦ g' ⁻¹' ( {f' i}) + have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg' have Z_subset_D i : Z i ⊆ D i := by intro z hz rw [mem_preimage, mem_singleton_iff] - obtain ⟨x, hx1, hx2⟩ := (mem_image _ _ _).mp hz - rw [←hx2] + obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm x - convert rfl - exact (eq_of_mem_singleton hx1).symm + simp_all have D_cover_univ : univ ⊆ (⋃ i, D i) := by intro y _ simp only [mem_iUnion] obtain ⟨s, hs⟩ := f'_surj (g' y) - use φ s - rw [mem_preimage, h1] + use s + rw [mem_preimage] exact hs.symm -- obtain clopens Z i ⊆ C i ⊆ D i with C i disjoint, covering Y obtain ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ := - clopen_partition_of_disjoint_closeds_in_clopens Y n Z D Z_closed D_clopen Z_subset_D Z_disj + clopen_partition_of_disjoint_closeds_in_clopens Z_closed D_clopen Z_subset_D Z_disj have C_cover_univ : ⋃ i, C i = univ := univ_subset_iff.mp (subset_trans D_cover_univ C_cover_D) -- define k to be the unique map sending C i to ψ i - have h_glue (i j : Fin n) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : ψ i = ψ j := by - by_cases hij : i = j - · exact congrArg ψ hij - · by_cases hij' : i < j - · exfalso - exact Set.disjoint_iff.mp (C_disj i j hij') (mem_inter hxi hxj) - · have hji' : j < i := lt_of_le_of_ne (not_lt.mp hij') (hij ∘ Eq.symm) - exfalso - exact Set.disjoint_iff.mp (C_disj j i hji') (mem_inter hxj hxi) - let k := liftCover C (λ i _ ↦ ψ i) h_glue C_cover_univ - -- now verify that k has the desired properties - have h_f'k_g' : f' ∘ k = g' := by + have h_glue (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : i = j := by + rw [Set.pairwiseDisjoint_iff] at C_disj + exact C_disj (by simp) (by simp) ⟨x, by grind⟩ + refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩ + · rw [IsLocallyConstant.iff_isOpen_fiber] + intro s + convert (C_clopen s).2 ext y - rw [Function.comp_apply] + simp [preimage_liftCover] + · ext y -- y is contained in C i for some i - have hy : y ∈ ⋃ i, C i := by - rw [C_cover_univ] - exact mem_univ y + have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ] obtain ⟨i, hi⟩ := mem_iUnion.mp hy - have hki : k y = ψ i := liftCover_of_mem hi - rw [hki] - exact symm (C_subset_D i hi) - have h_kf_g : k ∘ f = g := by - ext x - rw [Function.comp_apply] - let i := φ (g x) - have hfC : f x ∈ Z i := by - rw [mem_image] - exact ⟨x, symm (h1 (g x)), rfl⟩ - have hC : f x ∈ C i := Z_subset_C i hfC - have hki : k (f x) = ψ i := liftCover_of_mem hC - rw [hki] - exact (h1 (g x)) - have C_eq_fiber (i) : C i = k⁻¹' {ψ i} := by - ext y - constructor - · exact liftCover_of_mem - · rw [preimage_liftCover] - simp only [mem_iUnion, mem_image, mem_preimage, exists_and_left, - Subtype.exists, exists_prop, exists_eq_right, forall_exists_index, and_imp] - intro j hji hj - rw [Function.LeftInverse.injective h2 hji] at hj - exact hj - have h_cont : Continuous k := by - have h_loc_cst : IsLocallyConstant k := by - apply IsLocallyConstant.iff_isOpen_fiber.mpr - intro s - have hsi : s = ψ (φ s) := by rw [h1] - rw [hsi, ← C_eq_fiber] - exact (C_clopen (φ s)).2 - exact { isOpen_preimage := fun s _ ↦ h_loc_cst s } - exact ⟨k, h_cont, h_f'k_g', h_kf_g⟩ + simpa [liftCover_of_mem hi] using symm (C_subset_D i hi) + · ext x + simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)] -- categorically stated versions of key_extension_lemma @@ -284,11 +236,10 @@ lemma profinite_key_extension_lemma (X Y S T : Profinite.{u}) [Finite S] (f : X ⟶ Y) [Mono f] (f' : S ⟶ T) [Epi f'] (g : X ⟶ S) (g' : Y ⟶ T) (h_comm : f ≫ g' = g ≫ f') : ∃ k : Y ⟶ S, (k ≫ f' = g') ∧ (f ≫ k = g) := by - have h_comm' : (f ≫ g' : _ → _) = g ≫ f' := by simp_rw [h_comm] obtain ⟨k_fun, k_cont, h2, h3⟩ := key_extension_lemma X Y S T f f.hom.continuous ((CompHausLike.mono_iff_injective f).mp inferInstance) - f' ((Profinite.epi_iff_surjective f').mp inferInstance) - g g.hom.continuous g' g'.hom.continuous h_comm' + f' ((epi_iff_surjective f').mp inferInstance) + g g.hom.continuous g' g'.hom.continuous (by simp [← CompHausLike.coe_comp, h_comm]) exact ⟨TopCat.ofHom ⟨k_fun, k_cont⟩, ConcreteCategory.hom_ext_iff.mpr (congrFun h2), ConcreteCategory.hom_ext_iff.mpr (congrFun h3)⟩ @@ -300,14 +251,10 @@ lemma light_key_extension_lemma (X Y S T : LightProfinite.{u}) [hS : Finite S] (f : X ⟶ Y) [Mono f] (f' : S ⟶ T) [Epi f'] (g : X ⟶ S) (g' : Y ⟶ T) (h_comm : f ≫ g' = g ≫ f') : ∃ k : Y ⟶ S, (k ≫ f' = g') ∧ (f ≫ k = g) := by - haveI : Finite (lightToProfinite.obj S).toTop := hS -- help the instance inference - have h_comm' : (f ≫ g' : _ → _) = g ≫ f' := by simp_rw [h_comm] - obtain ⟨k_fun, k_cont, h2, h3⟩ := key_extension_lemma - (lightToProfinite.obj X) (lightToProfinite.obj Y) - (lightToProfinite.obj S) (lightToProfinite.obj T) + obtain ⟨k_fun, k_cont, h2, h3⟩ := key_extension_lemma X Y S T f f.hom.continuous ((CompHausLike.mono_iff_injective f).mp inferInstance) - f' ((LightProfinite.epi_iff_surjective f').mp inferInstance) - g g.hom.continuous g' g'.hom.continuous h_comm' + f' ((epi_iff_surjective f').mp inferInstance) + g g.hom.continuous g' g'.hom.continuous (by simp [← CompHausLike.coe_comp, h_comm]) exact ⟨TopCat.ofHom ⟨k_fun, k_cont⟩, ConcreteCategory.hom_ext_iff.mpr (congrFun h2), ConcreteCategory.hom_ext_iff.mpr (congrFun h3)⟩ @@ -319,7 +266,7 @@ namespace CompHausLike The map from a nonempty space to pt is (split) epi in a CompHausLike category of spaces -/ -instance {P : TopCat.{u} → Prop} [HasProp P PUnit.{u+1}] +instance {P : TopCat.{u} → Prop} [HasProp P PUnit.{u + 1}] (X : CompHausLike.{u} P) [Nonempty X] : IsSplitEpi (isTerminalPUnit.from X) := IsSplitEpi.mk' { section_ := const _ (Nonempty.some inferInstance), id := isTerminalPUnit.hom_ext _ _ } @@ -372,7 +319,7 @@ namespace LightProfinite -/ -instance injective_of_light (S : LightProfinite.{u}) [Nonempty S]: Injective S where +instance injective_of_light (S : LightProfinite.{u}) [Nonempty S] : Injective S where factors {X Y} g f h := by -- help the instance inference a bit haveI (n : ℕ) : Finite (S.component n) := @@ -401,33 +348,33 @@ instance injective_of_light (S : LightProfinite.{u}) [Nonempty S]: Injective S w -- h_up and h_down are the required commutativity properties have h_down (n : ℕ) : f ≫ (k_seq n).val = g ≫ S.proj n := (k_seq n).property have h_up (n : ℕ) : (k_seq (n+1)).val ≫ S.transitionMap n = (k_seq n).val := by - induction' n with n ih - · exact (Classical.choose_spec (h_step 0 k0 h_down0)).1 - · exact (Classical.choose_spec (h_step (n+1) (k_seq (n+1)).val (k_seq (n+1)).property)).1 + induction n with + | zero => exact (Classical.choose_spec (h_step 0 k0 h_down0)).1 + | succ n ih => + exact (Classical.choose_spec (h_step (n+1) (k_seq (n+1)).val (k_seq (n+1)).property)).1 let k_cone : Cone S.diagram := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ (k_seq n).val) (fun n ↦ (h_up n).symm) } -- now the induced map Y ⟶ S = lim S.component is the desired map use S.asLimit.lift k_cone let g_cone : Cone S.diagram := { pt := X, π := NatTrans.ofOpSequence (fun n ↦ g ≫ S.proj n) (fun n ↦ by - simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp] - exact congrArg _ (S.proj_comp_transitionMap n).symm) } + simpa using congrArg _ (S.proj_comp_transitionMap n).symm) } have hg : g = S.asLimit.lift g_cone := by apply S.asLimit.uniq g_cone intro n rw [NatTrans.ofOpSequence_app] rw [hg] have hlim : S.asLimit.lift (k_cone.extend f) = S.asLimit.lift g_cone := by - unfold Cone.extend + dsimp [Cone.extend] congr ext n - simp only [Cone.extensions_app, NatTrans.comp_app, Functor.const_map_app, - NatTrans.ofOpSequence_app] - erw [h_down] + simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down] rw [← hlim] apply S.asLimit.uniq (k_cone.extend f) intro n - simp only [Category.assoc, IsLimit.fac, Cone.extend_π, Cone.extensions_app, - NatTrans.comp_app, Functor.const_map_app] + simp + +instance injective_in_profinite_of_light (S : LightProfinite.{u}) [Nonempty S] : + Injective (lightToProfinite.obj S) := sorry end LightProfinite diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean index e22a6a7..b2a96fa 100644 --- a/LeanCondensed/Projects/LightSolid.lean +++ b/LeanCondensed/Projects/LightSolid.lean @@ -3,7 +3,13 @@ Copyright (c) 2024 Dagur Asgeirsson. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dagur Asgeirsson -/ -import LeanCondensed.Projects.InternallyProjective +import Mathlib.Condensed.Light.Epi +import LeanCondensed.Projects.MonoidalLinear +import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono +import LeanCondensed.Mathlib.Condensed.Light.Limits +import Mathlib.Condensed.Light.Monoidal +import Mathlib.CategoryTheory.Preadditive.Projective.Internal +import LeanCondensed.Mathlib.Condensed.Light.Monoidal import LeanCondensed.Projects.Proj import LeanCondensed.Projects.Sequence /-! @@ -61,7 +67,7 @@ variable (R : Type _) [CommRing R] instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := internallyProjective_ℕinfty _ -instance : InternallyProjective (P R) := ofRetract (P_retract _) inferInstance +instance : InternallyProjective (P R) := .ofRetract (P_retract _) variable (R : Type) [CommRing R] diff --git a/LeanCondensed/Projects/LocalizedMonoidal.lean b/LeanCondensed/Projects/LocalizedMonoidal.lean deleted file mode 100644 index c5ac661..0000000 --- a/LeanCondensed/Projects/LocalizedMonoidal.lean +++ /dev/null @@ -1,441 +0,0 @@ -/- -Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Dagur Asgeirsson --/ -import Mathlib.CategoryTheory.EffectiveEpi.RegularEpi -import Mathlib.CategoryTheory.Localization.Monoidal -import Mathlib.CategoryTheory.Monoidal.FunctorCategory -import Mathlib.Combinatorics.Quiver.ReflQuiver -import LeanCondensed.Mathlib.CategoryTheory.Localization.Bifunctor - -universe u - -namespace CategoryTheory - -open CategoryTheory Limits Opposite Monoidal MonoidalCategory Functor - -namespace Functor.Monoidal - -open Functor.LaxMonoidal Functor.OplaxMonoidal - -variable {C D : Type*} [Category C] [Category D] [MonoidalCategory C] [MonoidalCategory D] - (F : C ⥤ D) [F.Monoidal] - -@[reassoc] -theorem map_associator' (X Y Z : C) : - (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = - μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ - δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z := by - simp - -@[reassoc] -theorem map_associator_inv' (X Y Z : C) : - (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv = - F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ - δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z := by - rw [← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom, map_associator'] - simp - -end Functor.Monoidal - -open Functor.Monoidal - -section FunctorCategory - -set_option maxHeartbeats 300000 in -instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] - [MonoidalCategory E] (L : D ⥤ E) [L.LaxMonoidal] : - ((whiskeringRight C D E).obj L).LaxMonoidal where - ε := { app X := Functor.LaxMonoidal.ε L } - μ F G := { app X := Functor.LaxMonoidal.μ L (F.obj X) (G.obj X) } - -set_option maxHeartbeats 300000 in -instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] - [MonoidalCategory E] (L : D ⥤ E) [L.OplaxMonoidal] : - ((whiskeringRight C D E).obj L).OplaxMonoidal where - η := { app X := Functor.OplaxMonoidal.η L } - δ F G := { app X := Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X) } - oplax_left_unitality := by aesop -- `aesop_cat` fails for some reason - oplax_right_unitality := by aesop -- `aesop_cat` fails for some reason - -instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] - [MonoidalCategory E] (L : D ⥤ E) [L.Monoidal] : ((whiskeringRight C D E).obj L).Monoidal where - ε_η := by ext; exact Functor.Monoidal.ε_η _ - η_ε := by ext; exact Functor.Monoidal.η_ε _ - μ_δ _ _ := by ext; exact Functor.Monoidal.μ_δ _ _ _ - δ_μ _ _ := by ext; exact Functor.Monoidal.δ_μ _ _ _ - -end FunctorCategory - -section MonoidalFunctorTransport - -variable {C D : Type*} [Category C] [Category D] - [MonoidalCategory C] [MonoidalCategory D] - -def coreMonoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.CoreMonoidal where - εIso := εIso F ≪≫ i.app _ - μIso X Y := tensorIso (i.symm.app _) (i.symm.app _) ≪≫ μIso F X Y ≪≫ i.app _ - μIso_hom_natural_left _ _ := by simp [NatTrans.whiskerRight_app_tensor_app_assoc] - μIso_hom_natural_right _ _ := by simp [NatTrans.whiskerLeft_app_tensor_app_assoc] - associativity X Y Z := by - simp only [Iso.trans_hom, tensorIso_hom, Iso.app_hom, Iso.symm_hom, μIso_hom, comp_whiskerRight, - Category.assoc, MonoidalCategory.whiskerLeft_comp] - rw [← i.hom.naturality, map_associator_assoc, Functor.OplaxMonoidal.associativity_assoc, - whiskerLeft_δ_μ_assoc, δ_μ_assoc] - simp only [← Category.assoc] - congr 1 - slice_lhs 3 4 => - rw [← tensorHom_id, ← tensor_comp] - simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom] - simp only [Category.assoc] - rw [← whisker_exchange_assoc] - simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc, - Iso.inv_hom_id_assoc] - rw [← tensorHom_id, associator_naturality_assoc] - simp [← id_tensorHom, -tensorHom_id, ← tensor_comp_assoc] - left_unitality X := by - simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom, - μIso_hom, Category.assoc, ← tensor_comp_assoc, Iso.hom_inv_id_app, Category.comp_id, - Category.id_comp] - rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X), - ← Category.id_comp (Functor.LaxMonoidal.ε F), tensor_comp] - simp - right_unitality X := by - simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom, - μIso_hom, Category.assoc, ← tensor_comp_assoc, Category.id_comp, Iso.hom_inv_id_app, - Category.comp_id] - rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X), - ← Category.id_comp (Functor.LaxMonoidal.ε F), tensor_comp] - simp - -def monoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.Monoidal := - (coreMonoidalTransport i).toMonoidal - -end MonoidalFunctorTransport - -namespace Localization.Monoidal - -variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) (W : MorphismProperty C) - [MonoidalCategory C] - -variable [W.IsMonoidal] [L.IsLocalization W] {unit : D} (ε : L.obj (𝟙_ C) ≅ unit) - -local notation "L'" => toMonoidalCategory L W ε - -instance : (L').IsLocalization W := inferInstanceAs (L.IsLocalization W) - -variable {E : Type*} [Category E] [MonoidalCategory E] (F : LocalizedMonoidal L W ε ⥤ E) - [(L ⋙ F).Monoidal] - -instance : (L' ⋙ F).Monoidal := inferInstanceAs (L ⋙ F).Monoidal - -noncomputable instance : Lifting₂ L' L' W W - ((curriedTensor C) ⋙ (whiskeringRight C C E).obj (L' ⋙ F)) - (curriedTensor _ ⋙ (whiskeringRight _ _ _).obj F) := by - change (Lifting₂ L' L' W W - (((curriedTensor C) ⋙ (whiskeringRight C C D).obj L') ⋙ (whiskeringRight C D E).obj _) - (tensorBifunctor L W ε ⋙ (whiskeringRight _ _ _).obj F)) - apply (config := {allowSynthFailures := true}) Lifting₂.compRight - exact inferInstanceAs (Lifting₂ L L W W (curriedTensor C ⋙ (whiskeringRight C C D).obj L') - (Localization.lift₂ _ (isInvertedBy₂ L W ε) L L)) - -noncomputable instance : Lifting₂ L' L' W W - ((((whiskeringLeft₂ _).obj (L' ⋙ F)).obj (L' ⋙ F)).obj (curriedTensor E)) - ((((whiskeringLeft₂ _).obj F).obj F).obj (curriedTensor E)) where - iso' := Iso.refl _ - -noncomputable def μNatIso : ((((whiskeringLeft₂ _).obj F).obj F).obj (curriedTensor E)) ≅ - (curriedTensor _ ⋙ (whiskeringRight _ _ _).obj F) := by - refine lift₂NatIso L' L' W W - ((((whiskeringLeft₂ _).obj (L' ⋙ F)).obj (L' ⋙ F)).obj (curriedTensor E)) - ((curriedTensor C) ⋙ (whiskeringRight C C E).obj (L' ⋙ F)) - ((((whiskeringLeft₂ _).obj F).obj F).obj (curriedTensor E)) - (curriedTensor _ ⋙ (whiskeringRight _ _ _).obj F) - ?_ - refine NatIso.ofComponents (fun _ ↦ (NatIso.ofComponents (fun _ ↦ μIso (L' ⋙ F) _ _) ?_)) ?_ - · intros - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, Functor.comp_obj, curriedTensor_obj_obj, - whiskeringRight_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_map, Functor.comp_map, - curriedTensor_obj_map, μIso_hom] - change _ = _ ≫ (L' ⋙ F).map _ - rw [map_whiskerLeft] - simp - · intros - ext - simp only [Functor.comp_obj, whiskeringRight_obj_obj, curriedTensor_obj_obj, - whiskeringLeft₂_obj_obj_obj_obj_obj, Functor.comp_map, whiskeringRight_obj_map, - NatTrans.comp_app, Functor.whiskerRight_app, curriedTensor_map_app, NatIso.ofComponents_hom_app, - whiskeringLeft₂_obj_obj_obj_map_app] - change _ = _ ≫ (L' ⋙ F).map _ - rw [map_whiskerRight] - simp - -lemma μNatIso_hom_app_app (X Y : C) : - ((μNatIso L W ε F).hom.app ((L').obj X)).app ((L').obj Y) = - Functor.LaxMonoidal.μ (L' ⋙ F) X Y ≫ - F.map (Functor.OplaxMonoidal.δ L' X Y) := by - simp [μNatIso, lift₂NatIso, Lifting₂.iso, Lifting₂.iso'] - rfl - -lemma μNatIso_inv_app_app (X Y : C) : - ((μNatIso L W ε F).inv.app ((L').obj X)).app ((L').obj Y) = - F.map (Functor.LaxMonoidal.μ L' X Y) ≫ Functor.OplaxMonoidal.δ (L' ⋙ F) X Y := by - simp [μNatIso, lift₂NatIso, Lifting₂.iso, Lifting₂.iso'] - rfl - -@[reassoc] -lemma μNatIso_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ X') (g : Y ⟶ Y') : - (F.map f ⊗ₘ F.map g) ≫ ((μNatIso L W ε F).hom.app X').app Y' = - ((μNatIso L W ε F).hom.app X).app Y ≫ F.map (f ⊗ₘ g) := by - have := ((μNatIso L W ε F).hom.app X').naturality g - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_map, curriedTensor_obj_map, - Functor.comp_map] at this - rw [← Category.comp_id (F.map f), ← Category.id_comp (F.map g), MonoidalCategory.tensor_comp, - MonoidalCategory.id_tensorHom, Category.assoc, this] - have := (μNatIso L W ε F).hom.naturality f - apply NatTrans.congr_app at this - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, NatTrans.comp_app, whiskeringLeft₂_obj_obj_obj_map_app, - curriedTensor_map_app, Functor.comp_map, whiskeringRight_obj_map, - Functor.whiskerRight_app] at this - specialize this Y - rw [MonoidalCategory.tensorHom_id, ← Category.assoc, this] - rw [Category.assoc, ← F.map_comp] - congr - -lemma μNatIso_associativity_aux (X Y Z : C) : - ((μNatIso L W ε F).hom.app ((L').obj X ⊗ (L').obj Y)).app ((L').obj Z) = - (((μNatIso L W ε F).inv.app ((L').obj X)).app ((L').obj Y)) ▷ F.obj ((L').obj Z) ≫ - (α_ _ _ _).hom ≫ - (F.obj ((L').obj X)) ◁ (((μNatIso L W ε F).hom.app ((L').obj Y)).app ((L').obj Z)) ≫ - ((μNatIso L W ε F).hom.app ((L').obj X)).app ((L').obj Y ⊗ (L').obj Z) ≫ - F.map (α_ _ _ _).inv := by - simp [μNatIso_inv_app_app, μNatIso_hom_app_app] - have := ((μNatIso L W ε F).hom.app ((L').obj X)).naturality (Functor.LaxMonoidal.μ L' Y Z) - simp at this - change _ = _ ≫ (F.mapIso (Functor.mapIso _ (Functor.Monoidal.μIso L' Y Z))).hom at this - rw [← Iso.comp_inv_eq] at this - simp only [Functor.mapIso_inv, μIso_inv, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - Category.assoc] at this - change _ ≫ _ ≫ F.map ((L').obj X ◁ _) = _ at this - rw [← this] - simp [μNatIso_hom_app_app] - have := (μNatIso L W ε F).hom.naturality ((Functor.LaxMonoidal.μ L' X Y)) - apply NatTrans.congr_app at this - specialize this ((L').obj Z) - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, NatTrans.comp_app, - whiskeringLeft₂_obj_obj_obj_map_app, curriedTensor_map_app, Functor.comp_map, - whiskeringRight_obj_map, Functor.whiskerRight_app] at this - change _ = _ ≫ (F.mapIso ((Functor.mapIso _ (Functor.Monoidal.μIso L' _ _)).app _)).hom at this - rw [← Iso.comp_inv_eq] at this - simp only [Functor.mapIso_inv, Iso.app_inv, Category.assoc] at this - change _ ≫ _ ≫ F.map (_ ▷ (L').obj Z) = _ at this - rw [← this] - simp only [μNatIso_hom_app_app, Functor.comp_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - μIso_inv, Category.assoc] - slice_rhs 5 6 => - rw [← MonoidalCategory.whiskerLeft_comp, ← F.map_comp] - simp only [δ_μ, Functor.map_id, MonoidalCategory.whiskerLeft_id] - simp only [Category.id_comp, Category.assoc] - erw [map_associator' (L' ⋙ F)] - slice_rhs 2 3 => - simp only [Functor.comp_obj] - rw [← MonoidalCategory.comp_whiskerRight] - simp only [Functor.comp_obj, δ_μ, id_whiskerRight] - simp only [Functor.comp_obj, Category.id_comp, Functor.comp_map, Category.assoc, whiskerLeft_δ_μ, - Category.comp_id, δ_μ] - congr 2 - simp only [← F.map_comp] - simp - -set_option maxHeartbeats 800000 in -noncomputable def functorCoremonoidalOfComp : F.CoreMonoidal where - εIso := εIso (L ⋙ F) ≪≫ F.mapIso ε - μIso X Y := ((μNatIso L W ε F).app X).app Y - μIso_hom_natural_left f X := NatTrans.congr_app ((μNatIso L W ε F).hom.naturality f) X - μIso_hom_natural_right X f := ((μNatIso L W ε F).hom.app X).naturality f - associativity X Y Z := by - simp only [Functor.comp_obj, whiskeringRight_obj_obj, Iso.app_hom] - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - obtain ⟨y, ⟨eY⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ - obtain ⟨z, ⟨eZ⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Z) := ⟨_, ⟨(L').objObjPreimageIso Z⟩⟩ - suffices ((μNatIso L W ε F).hom.app ((L').obj x)).app ((L').obj y) ▷ F.obj ((L').obj z) ≫ - ((μNatIso L W ε F).hom.app (((L').obj x) ⊗ ((L').obj y))).app ((L').obj z) ≫ - F.map (α_ ((L').obj x) ((L').obj y) ((L').obj z)).hom = - (α_ (F.obj ((L').obj x)) (F.obj ((L').obj y)) (F.obj ((L').obj z))).hom ≫ - F.obj ((L').obj x) ◁ ((μNatIso L W ε F).hom.app ((L').obj y)).app ((L').obj z) ≫ - ((μNatIso L W ε F).hom.app ((L').obj x)).app (((L').obj y) ⊗ ((L').obj z)) by - refine Eq.trans ?_ ((((F.map eX.inv ⊗ₘ F.map eY.inv) ⊗ₘ F.map eZ.inv) ≫= this =≫ - (F.map (eX.hom ⊗ₘ eY.hom ⊗ₘ eZ.hom))).trans ?_) - · simp only [Category.assoc] - rw [← F.map_comp, ← associator_naturality, F.map_comp, ← μNatIso_naturality_assoc] - rw [← Category.comp_id (F.map eZ.inv), ← Category.id_comp (F.map eX.inv ⊗ₘ F.map eY.inv)] - rw [MonoidalCategory.tensor_comp, MonoidalCategory.tensorHom_id] - simp only [MonoidalCategory.id_tensorHom, whiskeringLeft₂_obj_obj_obj_obj_obj, - curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, Category.assoc] - rw [← comp_whiskerRight_assoc, μNatIso_naturality] - rw [MonoidalCategory.whisker_exchange_assoc] - simp only [← Category.assoc] - congr 2 - simp only [← MonoidalCategory.tensorHom_id, whiskeringLeft₂_obj_obj_obj_obj_obj, - curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, ← - MonoidalCategory.id_tensorHom, ← MonoidalCategory.tensor_comp, Category.comp_id, - Category.id_comp, Category.assoc, ← Functor.map_comp, Iso.inv_hom_id, Functor.map_id] - simp - · simp only [associator_conjugation, whiskeringLeft₂_obj_obj_obj_obj_obj, - curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, Category.assoc, - Iso.inv_hom_id_assoc, Iso.cancel_iso_hom_left] - rw [← μNatIso_naturality, ← MonoidalCategory.id_tensorHom, ← Functor.map_id] - simp only [Functor.comp_obj, whiskeringRight_obj_obj, curriedTensor_obj_obj, - ← MonoidalCategory.tensor_comp_assoc, ← Functor.map_comp, Category.id_comp, - Iso.inv_hom_id] - rw [μNatIso_naturality_assoc] - simp only [Functor.map_id, whiskeringRight_obj_obj, Functor.comp_obj, curriedTensor_obj_obj, - MonoidalCategory.id_tensorHom, MonoidalCategory.whiskerLeft_comp, Category.assoc] - slice_lhs 2 3 => - rw [← MonoidalCategory.whiskerLeft_comp, ← Functor.map_comp, - ← MonoidalCategory.tensor_comp] - simp only [Iso.inv_hom_id, MonoidalCategory.tensorHom_id, id_whiskerRight, Functor.map_id, - MonoidalCategory.whiskerLeft_id] - simp - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, μNatIso_hom_app_app, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - comp_whiskerRight, Category.assoc, MonoidalCategory.whiskerLeft_comp] - rw [μNatIso_associativity_aux] - simp only [Functor.comp_obj, whiskeringRight_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_obj, - curriedTensor_obj_obj, μNatIso_inv_app_app, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, - comp_whiskerRight, μNatIso_hom_app_app, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - MonoidalCategory.whiskerLeft_comp, Category.assoc, Iso.map_inv_hom_id, Category.comp_id] - simp only [← MonoidalCategory.tensorHom_id, ← MonoidalCategory.id_tensorHom, - Category.comp_id, ← MonoidalCategory.tensor_comp_assoc, - map_δ_μ_assoc, μ_δ, Functor.comp_obj] - simp - left_unitality X := by - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - simp only [Functor.comp_obj, Iso.trans_hom, εIso_hom, Functor.mapIso_hom, comp_whiskerRight, - whiskeringRight_obj_obj, Iso.app_hom, Category.assoc] - suffices (λ_ (F.obj ((L').obj x))).hom = Functor.LaxMonoidal.ε (L ⋙ F) ▷ F.obj ((L').obj x) ≫ - F.map ε.hom ▷ F.obj ((L').obj x) ≫ ((μNatIso L W ε F).hom.app (𝟙_ _)).app ((L').obj x) ≫ - F.map (λ_ ((L').obj x)).hom by - refine Eq.trans ?_ (((_ ◁ F.map eX.inv) ≫= this =≫ (F.map eX.hom)).trans ?_) - · simp - · simp only [id_whiskerLeft, Functor.comp_obj, whiskeringRight_obj_obj, - curriedTensor_obj_obj, Functor.LaxMonoidal.left_unitality, - Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, Functor.map_comp, Category.assoc] - slice_lhs 5 6 => - erw [← MonoidalCategory.tensorHom_id, ← Functor.map_id, μNatIso_naturality] - erw [μNatIso_hom_app_app] - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - MonoidalCategory.tensorHom_id, Category.assoc, ← Functor.map_comp] - have : Functor.LaxMonoidal.ε L' = ε.inv := rfl - rw [this, ← MonoidalCategory.comp_whiskerRight_assoc] - simp only [Iso.hom_inv_id, id_whiskerRight, Category.id_comp, δ_μ_assoc, Functor.map_comp] - slice_rhs 2 3 => - rw [← MonoidalCategory.tensorHom_id, ← Functor.map_id, μNatIso_naturality] - rw [@leftUnitor_inv_naturality_assoc] - rw [Iso.hom_inv_id_assoc, MonoidalCategory.whisker_exchange_assoc] - congr 1 - rw [← cancel_epi ((F.obj (L.obj (𝟙_ C))) ◁ F.map eX.hom)] - conv_rhs => rw [← MonoidalCategory.id_tensorHom, ← Functor.map_id, ← Category.assoc, - μNatIso_naturality_assoc] - erw [μNatIso_hom_app_app] - simp only [whiskeringRight_obj_obj, Functor.comp_obj, curriedTensor_obj_obj, - Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.id_tensorHom, - MonoidalCategory.tensorHom_id, Category.assoc] - rw [← MonoidalCategory.whiskerLeft_comp_assoc, ← Functor.map_comp] - simp only [Iso.hom_inv_id, Functor.map_id, MonoidalCategory.whiskerLeft_id, - Category.id_comp, ← Functor.map_comp] - congr 2 - rw [MonoidalCategory.whisker_exchange_assoc] - rw [@leftUnitor_naturality] - rw [@leftUnitor_hom_app, ε'] - slice_rhs 2 3 => - rw [← MonoidalCategory.comp_whiskerRight, Iso.hom_inv_id, whiskerRight_id] - simp only [Category.id_comp, Category.assoc] - change _ = _ ≫ Functor.LaxMonoidal.μ L' _ _ ≫ _ - simp - change (λ_ ((L' ⋙ F).obj x)).hom = _ - rw [Functor.LaxMonoidal.left_unitality (L' ⋙ F)] - simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj, curriedTensor_obj_obj, - Functor.LaxMonoidal.left_unitality, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal] - slice_rhs 2 4 => - erw [← MonoidalCategory.tensorHom_id, ← Functor.map_id, μNatIso_naturality] - erw [μNatIso_hom_app_app] - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - MonoidalCategory.tensorHom_id, Category.assoc, ← Functor.map_comp] - congr - rw [← Functor.LaxMonoidal.left_unitality L', leftUnitor_hom_app] - simp only [ε', hom_inv_whiskerRight_assoc] - change _ = _ ≫ Functor.LaxMonoidal.μ L' _ _ ≫ _ - simp - right_unitality X := by - obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ - simp only [Functor.comp_obj, Iso.trans_hom, εIso_hom, Functor.mapIso_hom, - MonoidalCategory.whiskerLeft_comp, whiskeringRight_obj_obj, Iso.app_hom, Category.assoc] - suffices (ρ_ (F.obj ((L').obj x))).hom = (F.obj ((L').obj x) ◁ Functor.LaxMonoidal.ε (L ⋙ F)) ≫ - (F.obj ((L').obj x) ◁ F.map ε.hom) ≫ ((μNatIso L W ε F).hom.app ((L').obj x)).app (𝟙_ _) ≫ - F.map (ρ_ ((L').obj x)).hom by - refine Eq.trans ?_ (((F.map eX.inv ▷ _) ≫= this =≫ (F.map eX.hom)).trans ?_) - · simp - · simp only [MonoidalCategory.whiskerRight_id, Functor.comp_obj, whiskeringRight_obj_obj, - curriedTensor_obj_obj, Functor.LaxMonoidal.right_unitality, - Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, Functor.map_comp, Category.assoc] - slice_lhs 5 6 => - erw [← MonoidalCategory.id_tensorHom, ← Functor.map_id, μNatIso_naturality] - erw [μNatIso_hom_app_app] - simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, - whiskeringRight_obj_obj, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, - MonoidalCategory.id_tensorHom, Category.assoc, ← Functor.map_comp] - have : Functor.LaxMonoidal.ε L' = ε.inv := rfl - rw [this, ← MonoidalCategory.whiskerLeft_comp_assoc] - simp only [Iso.hom_inv_id, Functor.map_comp] - slice_rhs 2 3 => - rw [← MonoidalCategory.id_tensorHom, ← Functor.map_id, μNatIso_naturality] - rw [@rightUnitor_inv_naturality_assoc] - rw [Iso.hom_inv_id_assoc, ← MonoidalCategory.whisker_exchange_assoc] - congr 1 - rw [← cancel_epi (F.map eX.hom ▷ (F.obj (L.obj (𝟙_ C))))] - conv_rhs => rw [← MonoidalCategory.tensorHom_id, ← Functor.map_id, ← Category.assoc, - μNatIso_naturality_assoc] - erw [μNatIso_hom_app_app] - simp only [whiskeringRight_obj_obj, Functor.comp_obj, curriedTensor_obj_obj, - Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.id_tensorHom, - MonoidalCategory.tensorHom_id, Category.assoc] - rw [← MonoidalCategory.comp_whiskerRight_assoc, ← Functor.map_comp] - simp only [Iso.hom_inv_id, Functor.map_id, id_whiskerRight, MonoidalCategory.whiskerLeft_id, - ← Functor.map_comp, Category.id_comp] - congr 2 - rw [← MonoidalCategory.whisker_exchange_assoc] - rw [@rightUnitor_naturality] - rw [@rightUnitor_hom_app, ε'] - slice_rhs 2 3 => - rw [← MonoidalCategory.whiskerLeft_comp, Iso.hom_inv_id, whiskerLeft_id] - simp only [Category.id_comp, Category.assoc] - change _ = _ ≫ Functor.LaxMonoidal.μ L' _ _ ≫ _ - erw [Category.id_comp] - change (ρ_ ((L' ⋙ F).obj x)).hom = _ - rw [Functor.LaxMonoidal.right_unitality (L' ⋙ F)] - simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj, curriedTensor_obj_obj, - Functor.LaxMonoidal.right_unitality, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, - Functor.map_comp] - slice_rhs 2 4 => - erw [← MonoidalCategory.id_tensorHom, ← Functor.map_id, μNatIso_naturality_assoc] - erw [μNatIso_hom_app_app] - simp only [whiskeringRight_obj_obj, Functor.comp_obj, curriedTensor_obj_obj, - Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.id_tensorHom, ← - Functor.map_comp, Category.assoc] - congr - rw [← Functor.LaxMonoidal.right_unitality L', rightUnitor_hom_app] - simp only [ε', whiskerLeft_hom_inv_assoc] - change _ = _ ≫ Functor.LaxMonoidal.μ L' _ _ ≫ _ - simp - -noncomputable def functorMonoidalOfComp : F.Monoidal := - (functorCoremonoidalOfComp L W ε F).toMonoidal - -end CategoryTheory.Localization.Monoidal diff --git a/LeanCondensed/Projects/MonoidalLinear.lean b/LeanCondensed/Projects/MonoidalLinear.lean index 07878a4..ff0b443 100644 --- a/LeanCondensed/Projects/MonoidalLinear.lean +++ b/LeanCondensed/Projects/MonoidalLinear.lean @@ -124,7 +124,7 @@ def monoidalLinear (A : Type u) [Ring A] [L.Additive] (R : D ⥤ C) [R.Full] [R. refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ (eX.hom ⊗ₘ eZ.hom)).trans ?_) · rw [← id_tensorHom, ← id_tensorHom, ← tensor_comp_assoc, ← Functor.map_smul, ← tensor_comp] simp [eZ, eY] - · simp [eX, eY, eZ, ← MonoidalCategory.id_tensorHom, ← MonoidalCategory.tensor_comp] + · simp [eX, eY, eZ, ← MonoidalCategory.id_tensorHom] rw [← Functor.map_smul, map_whiskerLeft', map_whiskerLeft'] simp · intro r Y Z f X @@ -136,7 +136,7 @@ def monoidalLinear (A : Type u) [Ring A] [L.Additive] (R : D ⥤ C) [R.Full] [R. refine Eq.trans ?_ (((eY.inv ⊗ₘ eX.inv) ≫= this =≫ (eZ.hom ⊗ₘ eX.hom)).trans ?_) · rw [← tensorHom_id, ← tensorHom_id, ← tensor_comp_assoc, ← Functor.map_smul, ← tensor_comp] simp [eZ, eY] - · simp [eX, eY, eZ, ← MonoidalCategory.tensorHom_id, ← MonoidalCategory.tensor_comp] + · simp [eX, eY, eZ, ← MonoidalCategory.tensorHom_id] rw [← Functor.map_smul, map_whiskerRight', map_whiskerRight'] simp diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index 9f7889f..4cb4375 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -3,7 +3,8 @@ Copyright (c) 2025 Jonas van der Schaaf. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jonas van der Schaaf -/ -import LeanCondensed.Projects.InternallyProjective +-- import LeanCondensed.Projects.InternallyProjective +import Mathlib.Condensed.Light.InternallyProjective import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.PreservesCoprod import LeanCondensed.Projects.Epi diff --git a/LeanCondensed/Projects/SheafMonoidal.lean b/LeanCondensed/Projects/SheafMonoidal.lean index 0be9898..8bc9328 100644 --- a/LeanCondensed/Projects/SheafMonoidal.lean +++ b/LeanCondensed/Projects/SheafMonoidal.lean @@ -5,11 +5,11 @@ Authors: Dagur Asgeirsson -/ import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced import Mathlib.CategoryTheory.Limits.Shapes.Countable +import Mathlib.CategoryTheory.Localization.Monoidal.Functor import Mathlib.CategoryTheory.Sites.CartesianMonoidal import Mathlib.CategoryTheory.Sites.LeftExact import Mathlib.CategoryTheory.Sites.Monoidal import Mathlib.CategoryTheory.Sites.PreservesSheafification -import LeanCondensed.Projects.LocalizedMonoidal universe v u @@ -38,10 +38,15 @@ variable {A B : Type*} [Category A] [Category B] attribute [local instance] monoidalCategory noncomputable instance : (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal := - monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm + Functor.Monoidal.transport (presheafToSheafCompComposeAndSheafifyIso J F).symm + +noncomputable instance : Localization.Lifting (presheafToSheaf J A) J.W + (presheafToSheaf _ _ ⋙ composeAndSheafify J F) (composeAndSheafify J F) where + iso := Iso.refl _ noncomputable instance : (composeAndSheafify J F).Monoidal := - Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (Iso.refl _) _ + Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (composeAndSheafify J F) + (presheafToSheaf _ _ ⋙ composeAndSheafify J F) --(Iso.refl _) _ end @@ -56,7 +61,7 @@ noncomputable instance : letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal := letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A - monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm + Functor.Monoidal.transport (presheafToSheafCompComposeAndSheafifyIso J F).symm noncomputable instance foo : letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A diff --git a/lake-manifest.json b/lake-manifest.json index d77f226..3f29673 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "87bad3eb59d315b0cad61e2508d7228cf66e5cd1", + "rev": "07946e860d2f824f658fe62db9a3b010e953cd60", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493", + "rev": "74835c84b38e4070b8240a063c6417c767e551ae", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f", + "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.71", + "inputRev": "v0.0.82", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0", + "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f85ad59c9b60647ef736719c23edd4578f723806", + "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d", + "rev": "f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf", + "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.26.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "LeanCondensed", diff --git a/lean-toolchain b/lean-toolchain index 27770b5..7035713 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.23.0-rc2 \ No newline at end of file +leanprover/lean4:v4.26.0-rc2 \ No newline at end of file