From 239d882c4fb58361ee8b3b39fb2091320edef10a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sat, 13 Aug 2022 07:30:14 +0000 Subject: [PATCH] refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036) This PR makes a distinction between the class `is_split_epi f` which is a `Prop` and `split_epi f` which contains the datum of a section of `f`. --- .../adjunction/reflective.lean | 6 +- src/category_theory/closed/cartesian.lean | 4 +- src/category_theory/closed/ideal.lean | 4 +- src/category_theory/epi_mono.lean | 154 +++++++++++++----- src/category_theory/functor/epi_mono.lean | 14 +- src/category_theory/generator.lean | 5 +- .../limits/constructions/weakly_initial.lean | 2 +- .../limits/preserves/shapes/biproducts.lean | 46 ++++-- .../limits/shapes/binary_products.lean | 4 +- .../limits/shapes/biproducts.lean | 64 ++++---- .../limits/shapes/equalizers.lean | 27 +-- .../limits/shapes/regular_mono.lean | 14 +- .../limits/shapes/terminal.lean | 20 +-- .../limits/shapes/zero_morphisms.lean | 32 ++-- src/category_theory/simple.lean | 7 +- src/category_theory/sites/sheaf_of_types.lean | 2 +- src/category_theory/sites/sieves.lean | 12 +- src/category_theory/types.lean | 4 +- 18 files changed, 247 insertions(+), 174 deletions(-) diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean index 39f172553e620..3febb0a8d88f7 100644 --- a/src/category_theory/adjunction/reflective.lean +++ b/src/category_theory/adjunction/reflective.lean @@ -89,8 +89,8 @@ lemma mem_ess_image_of_unit_is_iso [is_right_adjoint i] (A : C) ⟨(left_adjoint i).obj A, ⟨(as_iso ((of_right_adjoint i).unit.app A)).symm⟩⟩ /-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/ -lemma mem_ess_image_of_unit_split_mono [reflective i] {A : C} - [split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := +lemma mem_ess_image_of_unit_is_split_mono [reflective i] {A : C} + [is_split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := begin let η : 𝟭 C ⟶ left_adjoint i ⋙ i := (of_right_adjoint i).unit, haveI : is_iso (η.app (i.obj ((left_adjoint i).obj A))) := (i.obj_mem_ess_image _).unit_is_iso, @@ -99,7 +99,7 @@ begin rw (show retraction _ ≫ η.app A = _, from η.naturality (retraction (η.app A))), apply epi_comp (η.app (i.obj ((left_adjoint i).obj A))) }, resetI, - haveI := is_iso_of_epi_of_split_mono (η.app A), + haveI := is_iso_of_epi_of_is_split_mono (η.app A), exact mem_ess_image_of_unit_is_iso A, end diff --git a/src/category_theory/closed/cartesian.lean b/src/category_theory/closed/cartesian.lean index b3ea9b725fd7c..848aeeb9213a2 100644 --- a/src/category_theory/closed/cartesian.lean +++ b/src/category_theory/closed/cartesian.lean @@ -306,8 +306,8 @@ lemma strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f := begin haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _, rw [zero_mul_hom, prod.lift_snd] at _inst, - haveI: split_epi f := ⟨t.to _, t.hom_ext _ _⟩, - apply is_iso_of_mono_of_split_epi + haveI: is_split_epi f := is_split_epi.mk' ⟨t.to _, t.hom_ext _ _⟩, + apply is_iso_of_mono_of_is_split_epi end instance to_initial_is_iso [has_initial C] (f : A ⟶ ⊥_ C) : is_iso f := diff --git a/src/category_theory/closed/ideal.lean b/src/category_theory/closed/ideal.lean index 50ba92dc0dbc4..7d8c309392d38 100644 --- a/src/category_theory/closed/ideal.lean +++ b/src/category_theory/closed/ideal.lean @@ -143,8 +143,8 @@ begin ir.hom_equiv_apply_eq, assoc, assoc, prod_comparison_natural_assoc, L.map_id, ← prod.map_id_comp_assoc, ir.left_triangle_components, prod.map_id_id, id_comp], apply is_iso.hom_inv_id_assoc }, - haveI : split_mono (η.app (A ⟹ i.obj B)) := ⟨_, this⟩, - apply mem_ess_image_of_unit_split_mono, + haveI : is_split_mono (η.app (A ⟹ i.obj B)) := is_split_mono.mk' ⟨_, this⟩, + apply mem_ess_image_of_unit_is_split_mono, end variables [exponential_ideal i] diff --git a/src/category_theory/epi_mono.lean b/src/category_theory/epi_mono.lean index d4cbb01d8edc6..ff2d5f37c00a9 100644 --- a/src/category_theory/epi_mono.lean +++ b/src/category_theory/epi_mono.lean @@ -33,94 +33,146 @@ instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op := ⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩ /-- -A split monomorphism is a morphism `f : X ⟶ Y` admitting a retraction `retraction f : Y ⟶ X` +A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X` such that `f ≫ retraction f = 𝟙 X`. Every split monomorphism is a monomorphism. -/ -@[ext] -class split_mono {X Y : C} (f : X ⟶ Y) := +@[ext, nolint has_nonempty_instance] +structure split_mono {X Y : C} (f : X ⟶ Y) := (retraction : Y ⟶ X) (id' : f ≫ retraction = 𝟙 X . obviously) +restate_axiom split_mono.id' +attribute [simp, reassoc] split_mono.id + +/-- `is_split_mono f` is the assertion that `f` admits a retraction -/ +class is_split_mono {X Y : C} (f : X ⟶ Y) : Prop := +(exists_split_mono : nonempty (split_mono f)) + +/-- A constructor for `is_split_mono f` taking a `split_mono f` as an argument -/ +lemma is_split_mono.mk' {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : + is_split_mono f := ⟨nonempty.intro sm⟩ + /-- -A split epimorphism is a morphism `f : X ⟶ Y` admitting a section `section_ f : Y ⟶ X` +A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X` such that `section_ f ≫ f = 𝟙 Y`. (Note that `section` is a reserved keyword, so we append an underscore.) Every split epimorphism is an epimorphism. -/ -@[ext] -class split_epi {X Y : C} (f : X ⟶ Y) := +@[ext, nolint has_nonempty_instance] +structure split_epi {X Y : C} (f : X ⟶ Y) := (section_ : Y ⟶ X) (id' : section_ ≫ f = 𝟙 Y . obviously) +restate_axiom split_epi.id' +attribute [simp, reassoc] split_epi.id + +/-- `is_split_epi f` is the assertion that `f` admits a section -/ +class is_split_epi {X Y : C} (f : X ⟶ Y) : Prop := +(exists_split_epi : nonempty (split_epi f)) + +/-- A constructor for `is_split_epi f` taking a `split_epi f` as an argument -/ +lemma is_split_epi.mk' {X Y : C} {f : X ⟶ Y} (se : split_epi f) : + is_split_epi f := ⟨nonempty.intro se⟩ + /-- The chosen retraction of a split monomorphism. -/ -def retraction {X Y : C} (f : X ⟶ Y) [split_mono f] : Y ⟶ X := split_mono.retraction f +noncomputable def retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : Y ⟶ X := +hf.exists_split_mono.some.retraction + @[simp, reassoc] -lemma split_mono.id {X Y : C} (f : X ⟶ Y) [split_mono f] : f ≫ retraction f = 𝟙 X := -split_mono.id' +lemma is_split_mono.id {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : f ≫ retraction f = 𝟙 X := +hf.exists_split_mono.some.id + +/-- The retraction of a split monomorphism has an obvious section. -/ +def split_mono.split_epi {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : split_epi (sm.retraction) := +{ section_ := f, } + /-- The retraction of a split monomorphism is itself a split epimorphism. -/ -instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi (retraction f) := -{ section_ := f } +instance retraction_is_split_epi {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : +is_split_epi (retraction f) := +is_split_epi.mk' (split_mono.split_epi _) /-- A split mono which is epi is an iso. -/ -lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f := +lemma is_iso_of_epi_of_is_split_mono {X Y : C} (f : X ⟶ Y) [is_split_mono f] [epi f] : is_iso f := ⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩ /-- The chosen section of a split epimorphism. (Note that `section` is a reserved keyword, so we append an underscore.) -/ -def section_ {X Y : C} (f : X ⟶ Y) [split_epi f] : Y ⟶ X := split_epi.section_ f +noncomputable def section_ {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : Y ⟶ X := +hf.exists_split_epi.some.section_ + @[simp, reassoc] -lemma split_epi.id {X Y : C} (f : X ⟶ Y) [split_epi f] : section_ f ≫ f = 𝟙 Y := -split_epi.id' +lemma is_split_epi.id {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : section_ f ≫ f = 𝟙 Y := +hf.exists_split_epi.some.id + +/-- The section of a split epimorphism has an obvious retraction. -/ +def split_epi.split_mono {X Y : C} {f : X ⟶ Y} (se : split_epi f) : split_mono (se.section_) := +{ retraction := f, } + /-- The section of a split epimorphism is itself a split monomorphism. -/ -instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (section_ f) := -{ retraction := f } +instance section_is_split_mono {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : + is_split_mono (section_ f) := +is_split_mono.mk' (split_epi.split_mono _) /-- A split epi which is mono is an iso. -/ -lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f := +lemma is_iso_of_mono_of_is_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [is_split_epi f] : is_iso f := ⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩ /-- Every iso is a split mono. -/ @[priority 100] -noncomputable -instance split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_mono f := -{ retraction := inv f } +instance is_split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_mono f := +is_split_mono.mk' { retraction := inv f } /-- Every iso is a split epi. -/ @[priority 100] -noncomputable -instance split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_epi f := -{ section_ := inv f } +instance is_split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_epi f := +is_split_epi.mk' { section_ := inv f } + +lemma split_mono.mono {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : mono f := +{ right_cancellation := λ Z g h w, begin replace w := w =≫ sm.retraction, simpa using w, end } /-- Every split mono is a mono. -/ @[priority 100] -instance split_mono.mono {X Y : C} (f : X ⟶ Y) [split_mono f] : mono f := -{ right_cancellation := λ Z g h w, begin replace w := w =≫ retraction f, simpa using w, end } +instance is_split_mono.mono {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : mono f := +hf.exists_split_mono.some.mono + +lemma split_epi.epi {X Y : C} {f : X ⟶ Y} (se : split_epi f) : epi f := +{ left_cancellation := λ Z g h w, begin replace w := se.section_ ≫= w, simpa using w, end } /-- Every split epi is an epi. -/ @[priority 100] -instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f := -{ left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end } +instance is_split_epi.epi {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : epi f := +hf.exists_split_epi.some.epi + +/-- Every split mono whose retraction is mono is an iso. -/ +lemma is_iso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : split_mono f) + [mono $ hf.retraction] : is_iso f := +⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id $ hf.retraction).mp (by simp)⟩⟩⟩ /-- Every split mono whose retraction is mono is an iso. -/ -lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f] - : is_iso f := -⟨⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩⟩ +lemma is_iso.of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] + [hf' : mono $ retraction f] : is_iso f := +@is_iso.of_mono_retraction' _ _ _ _ _ hf.exists_split_mono.some hf' /-- Every split epi whose section is epi is an iso. -/ -lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f] - : is_iso f := -⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩ +lemma is_iso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : split_epi f) + [epi $ hf.section_] : is_iso f := +⟨⟨hf.section_, ⟨(cancel_epi_id $ hf.section_).mp (by simp), by simp⟩⟩⟩ + +/-- Every split epi whose section is epi is an iso. -/ +lemma is_iso.of_epi_section {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] + [hf' : epi $ section_ f] : is_iso f := +@is_iso.of_epi_section' _ _ _ _ _ hf.exists_split_epi.some hf' /-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/ -- FIXME this has unnecessarily become noncomputable! noncomputable def groupoid.of_trunc_split_mono - (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) : + (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (is_split_mono f)) : groupoid.{v₁} C := begin apply groupoid.of_is_iso, @@ -135,36 +187,48 @@ variables (C) /-- A split mono category is a category in which every monomorphism is split. -/ class split_mono_category := -(split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], split_mono f) +(is_split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], is_split_mono f) /-- A split epi category is a category in which every epimorphism is split. -/ class split_epi_category := -(split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], split_epi f) +(is_split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], is_split_epi f) end /-- In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop. -/ -def split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] : split_mono f := -split_mono_category.split_mono_of_mono _ +lemma is_split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] : + is_split_mono f := +split_mono_category.is_split_mono_of_mono _ /-- In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop. -/ -def split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] : split_epi f := -split_epi_category.split_epi_of_epi _ +lemma is_split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] : + is_split_epi f := split_epi_category.is_split_epi_of_epi _ section variables {D : Type u₂} [category.{v₂} D] /-- Split monomorphisms are also absolute monomorphisms. -/ -instance {X Y : C} (f : X ⟶ Y) [split_mono f] (F : C ⥤ D) : split_mono (F.map f) := -{ retraction := F.map (retraction f), +@[simps] +def split_mono.map {X Y : C} {f : X ⟶ Y} (sm : split_mono f) (F : C ⥤ D ) : + split_mono (F.map f) := +{ retraction := F.map (sm.retraction), id' := by { rw [←functor.map_comp, split_mono.id, functor.map_id], } } /-- Split epimorphisms are also absolute epimorphisms. -/ -instance {X Y : C} (f : X ⟶ Y) [split_epi f] (F : C ⥤ D) : split_epi (F.map f) := -{ section_ := F.map (section_ f), +@[simps] +def split_epi.map {X Y : C} {f : X ⟶ Y} (se : split_epi f) (F : C ⥤ D ) : + split_epi (F.map f) := +{ section_ := F.map (se.section_), id' := by { rw [←functor.map_comp, split_epi.id, functor.map_id], } } + +instance {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] (F : C ⥤ D) : is_split_mono (F.map f) := +is_split_mono.mk' (hf.exists_split_mono.some.map F) + +instance {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] (F : C ⥤ D) : is_split_epi (F.map f) := +is_split_epi.mk' (hf.exists_split_epi.some.map F) + end end category_theory diff --git a/src/category_theory/functor/epi_mono.lean b/src/category_theory/functor/epi_mono.lean index 25f127e04fd1b..cb3bff689fb2a 100644 --- a/src/category_theory/functor/epi_mono.lean +++ b/src/category_theory/functor/epi_mono.lean @@ -171,19 +171,9 @@ section variables (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) -/-- Split epimorphisms are preserved by the application of any functor. -/ -@[simps] -def map_split_epi (s : split_epi f) : split_epi (F.map f) := -⟨F.map s.section_, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_epi.id, }⟩ - -/-- Split monomorphisms are preserved by the application of any functor. -/ -@[simps] -def map_split_mono (s : split_mono f) : split_mono (F.map f) := -⟨F.map s.retraction, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_mono.id, }⟩ - /-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/ def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f) := -{ to_fun := F.map_split_epi f, +{ to_fun := λ f, f.map F, inv_fun := λ s, begin refine ⟨F.preimage s.section_, _⟩, apply F.map_injective, @@ -195,7 +185,7 @@ def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f) /-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/ def split_mono_equiv [full F] [faithful F] : split_mono f ≃ split_mono (F.map f) := -{ to_fun := F.map_split_mono f, +{ to_fun := λ f, f.map F, inv_fun := λ s, begin refine ⟨F.preimage s.retraction, _⟩, apply F.map_injective, diff --git a/src/category_theory/generator.lean b/src/category_theory/generator.lean index 75053d15e0443..e398a80921da1 100644 --- a/src/category_theory/generator.lean +++ b/src/category_theory/generator.lean @@ -278,9 +278,10 @@ begin haveI : mono t := (is_coseparating_iff_mono 𝒢).1 h𝒢 A, exact subobject.of_le_mk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd }, { generalize : default = g, - suffices : split_epi (equalizer.ι f g), + suffices : is_split_epi (equalizer.ι f g), { exactI eq_of_epi_equalizer }, - exact ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _) bot_le, by { ext, simp }⟩ } + exact is_split_epi.mk' ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _) + bot_le, by { ext, simp }⟩ } end /-- An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered diff --git a/src/category_theory/limits/constructions/weakly_initial.lean b/src/category_theory/limits/constructions/weakly_initial.lean index 8dc5249777940..2995d575ff221 100644 --- a/src/category_theory/limits/constructions/weakly_initial.lean +++ b/src/category_theory/limits/constructions/weakly_initial.lean @@ -56,7 +56,7 @@ begin { rw [category.assoc, category.assoc], apply wide_equalizer.condition (id : endos → endos) (h ≫ e ≫ i) }, rw [category.comp_id, cancel_mono_id i] at this, - haveI : split_epi e := ⟨i ≫ h, this⟩, + haveI : is_split_epi e := is_split_epi.mk' ⟨i ≫ h, this⟩, rw ←cancel_epi e, apply equalizer.condition }, exactI has_initial_of_unique (wide_equalizer (id : endos → endos)), diff --git a/src/category_theory/limits/preserves/shapes/biproducts.lean b/src/category_theory/limits/preserves/shapes/biproducts.lean index 9d6601853f409..5727f969e1b36 100644 --- a/src/category_theory/limits/preserves/shapes/biproducts.lean +++ b/src/category_theory/limits/preserves/shapes/biproducts.lean @@ -216,17 +216,21 @@ variables [preserves_zero_morphisms F] biproduct_comparison' F f ≫ biproduct_comparison F f = 𝟙 (⨁ (F.obj ∘ f)) := by { classical, ext, simp [biproduct.ι_π, ← functor.map_comp, eq_to_hom_map] } -instance : split_epi (biproduct_comparison F f) := +/-- `biproduct_comparison F f` is a split epimorphism. -/ +@[simps] +def split_epi_biproduct_comparison : split_epi (biproduct_comparison F f) := ⟨biproduct_comparison' F f⟩ -@[simp] lemma section_biproduct_comparison : - section_ (biproduct_comparison F f) = biproduct_comparison' F f := rfl +instance : is_split_epi (biproduct_comparison F f) := +is_split_epi.mk' (split_epi_biproduct_comparison F f) -instance : split_mono (biproduct_comparison' F f) := +/-- `biproduct_comparison' F f` is a split monomorphism. -/ +@[simps] +def split_mono_biproduct_comparison' : split_mono (biproduct_comparison' F f) := ⟨biproduct_comparison F f⟩ -@[simp] lemma retraction_biproduct_comparison' : - retraction (biproduct_comparison' F f) = biproduct_comparison F f := rfl +instance : is_split_mono (biproduct_comparison' F f) := +is_split_mono.mk' (split_mono_biproduct_comparison' F f) end @@ -290,17 +294,21 @@ variables [preserves_zero_morphisms F] biprod_comparison' F X Y ≫ biprod_comparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y) := by { ext; simp [← functor.map_comp] } -instance : split_epi (biprod_comparison F X Y) := +/-- `biprod_comparison F X Y` is a split epi. -/ +@[simps] +def split_epi_biprod_comparison : split_epi (biprod_comparison F X Y) := ⟨biprod_comparison' F X Y⟩ -@[simp] lemma section_biprod_comparison : - section_ (biprod_comparison F X Y) = biprod_comparison' F X Y := rfl +instance : is_split_epi (biprod_comparison F X Y) := +is_split_epi.mk' (split_epi_biprod_comparison F X Y) -instance : split_mono (biprod_comparison' F X Y) := +/-- `biprod_comparison' F X Y` is a split mono. -/ +@[simps] +def split_mono_biprod_comparison' : split_mono (biprod_comparison' F X Y) := ⟨biprod_comparison F X Y⟩ -@[simp] lemma retraction_biprod_comparison' : - retraction (biprod_comparison' F X Y) = biprod_comparison F X Y := rfl +instance : is_split_mono (biprod_comparison' F X Y) := +is_split_mono.mk' (split_mono_biprod_comparison' F X Y) end @@ -421,7 +429,7 @@ begin have : pi_comparison F f = (F.map_iso (biproduct.iso_product f)).inv ≫ biproduct_comparison F f ≫ (biproduct.iso_product _).hom, { ext, convert pi_comparison_comp_π F f j.as; simp [← functor.map_comp] }, - haveI : is_iso (biproduct_comparison F f) := is_iso_of_mono_of_split_epi _, + haveI : is_iso (biproduct_comparison F f) := is_iso_of_mono_of_is_split_epi _, haveI : is_iso (pi_comparison F f) := by { rw this, apply_instance }, haveI := preserves_product.of_iso_comparison F f, apply preserves_biproduct_of_preserves_product @@ -432,8 +440,9 @@ end def preserves_biproduct_of_epi_biproduct_comparison' {f : J → C} [has_biproduct f] [has_biproduct (F.obj ∘ f)] [epi (biproduct_comparison' F f)] : preserves_biproduct f F := begin - haveI : epi (section_ (biproduct_comparison F f)) := by simpa, - haveI : is_iso (biproduct_comparison F f) := is_iso.of_epi_section, + haveI : epi ((split_epi_biproduct_comparison F f).section_) := by simpa, + haveI : is_iso (biproduct_comparison F f) := is_iso.of_epi_section' + (split_epi_biproduct_comparison F f), apply preserves_biproduct_of_mono_biproduct_comparison end @@ -519,7 +528,7 @@ def preserves_binary_biproduct_of_mono_biprod_comparison {X Y : C} [has_binary_b begin have : prod_comparison F X Y = (F.map_iso (biprod.iso_prod X Y)).inv ≫ biprod_comparison F X Y ≫ (biprod.iso_prod _ _).hom := by { ext; simp [← functor.map_comp] }, - haveI : is_iso (biprod_comparison F X Y) := is_iso_of_mono_of_split_epi _, + haveI : is_iso (biprod_comparison F X Y) := is_iso_of_mono_of_is_split_epi _, haveI : is_iso (prod_comparison F X Y) := by { rw this, apply_instance }, haveI := preserves_limit_pair.of_iso_prod_comparison F X Y, apply preserves_binary_biproduct_of_preserves_binary_product @@ -531,8 +540,9 @@ def preserves_binary_biproduct_of_epi_biprod_comparison' {X Y : C} [has_binary_b [has_binary_biproduct (F.obj X) (F.obj Y)] [epi (biprod_comparison' F X Y)] : preserves_binary_biproduct X Y F := begin - haveI : epi (section_ (biprod_comparison F X Y)) := by simpa, - haveI : is_iso (biprod_comparison F X Y) := is_iso.of_epi_section, + haveI : epi ((split_epi_biprod_comparison F X Y).section_) := by simpa, + haveI : is_iso (biprod_comparison F X Y) := is_iso.of_epi_section' + (split_epi_biprod_comparison F X Y), apply preserves_binary_biproduct_of_mono_biprod_comparison end diff --git a/src/category_theory/limits/shapes/binary_products.lean b/src/category_theory/limits/shapes/binary_products.lean index 663d82320607f..76698c5a4a482 100644 --- a/src/category_theory/limits/shapes/binary_products.lean +++ b/src/category_theory/limits/shapes/binary_products.lean @@ -471,8 +471,8 @@ lemma prod.diag_map_fst_snd_comp [has_limits_of_shape (discrete walking_pair) C diag (X ⨯ X') ≫ prod.map (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g' := by simp -instance {X : C} [has_binary_product X X] : split_mono (diag X) := -{ retraction := prod.fst } +instance {X : C} [has_binary_product X X] : is_split_mono (diag X) := +is_split_mono.mk' { retraction := prod.fst } end prod_lemmas diff --git a/src/category_theory/limits/shapes/biproducts.lean b/src/category_theory/limits/shapes/biproducts.lean index 7613d92dc0690..6e3f996250607 100644 --- a/src/category_theory/limits/shapes/biproducts.lean +++ b/src/category_theory/limits/shapes/biproducts.lean @@ -665,10 +665,12 @@ end finite_biproducts variables {J : Type w} {C : Type u} [category.{v} C] [has_zero_morphisms C] -instance biproduct.ι_mono (f : J → C) [has_biproduct f] (b : J) : split_mono (biproduct.ι f b) := +instance biproduct.ι_mono (f : J → C) [has_biproduct f] (b : J) : + is_split_mono (biproduct.ι f b) := is_split_mono.mk' { retraction := biproduct.desc $ pi.single b _ } -instance biproduct.π_epi (f : J → C) [has_biproduct f] (b : J) : split_epi (biproduct.π f b) := +instance biproduct.π_epi (f : J → C) [has_biproduct f] (b : J) : + is_split_epi (biproduct.π f b) := is_split_epi.mk' { section_ := biproduct.lift $ pi.single b _ } /-- Auxiliary lemma for `biproduct.unique_up_to_iso`. -/ @@ -802,13 +804,17 @@ rfl lemma binary_cofan_inr_to_cocone (c : binary_bicone P Q) : binary_cofan.inr c.to_cocone = c.inr := rfl -instance (c : binary_bicone P Q) : split_mono c.inl := { retraction := c.fst, id' := c.inl_fst } +instance (c : binary_bicone P Q) : is_split_mono c.inl := +is_split_mono.mk' { retraction := c.fst, id' := c.inl_fst } -instance (c : binary_bicone P Q) : split_mono c.inr := { retraction := c.snd, id' := c.inr_snd } +instance (c : binary_bicone P Q) : is_split_mono c.inr := +is_split_mono.mk' { retraction := c.snd, id' := c.inr_snd } -instance (c : binary_bicone P Q) : split_epi c.fst := { section_ := c.inl, id' := c.inl_fst } +instance (c : binary_bicone P Q) : is_split_epi c.fst := +is_split_epi.mk' { section_ := c.inl, id' := c.inl_fst } -instance (c : binary_bicone P Q) : split_epi c.snd := { section_ := c.inr, id' := c.inr_snd } +instance (c : binary_bicone P Q) : is_split_epi c.snd := +is_split_epi.mk' { section_ := c.inr, id' := c.inr_snd } /-- Convert a `binary_bicone` into a `bicone` over a pair. -/ @[simps] @@ -1146,20 +1152,20 @@ begin end instance biprod.inl_mono {X Y : C} [has_binary_biproduct X Y] : - split_mono (biprod.inl : X ⟶ X ⊞ Y) := -{ retraction := biprod.fst } + is_split_mono (biprod.inl : X ⟶ X ⊞ Y) := +is_split_mono.mk' { retraction := biprod.fst } instance biprod.inr_mono {X Y : C} [has_binary_biproduct X Y] : - split_mono (biprod.inr : Y ⟶ X ⊞ Y) := -{ retraction := biprod.snd } + is_split_mono (biprod.inr : Y ⟶ X ⊞ Y) := +is_split_mono.mk' { retraction := biprod.snd } instance biprod.fst_epi {X Y : C} [has_binary_biproduct X Y] : - split_epi (biprod.fst : X ⊞ Y ⟶ X) := -{ section_ := biprod.inl } + is_split_epi (biprod.fst : X ⊞ Y ⟶ X) := +is_split_epi.mk' { section_ := biprod.inl } instance biprod.snd_epi {X Y : C} [has_binary_biproduct X Y] : - split_epi (biprod.snd : X ⊞ Y ⟶ Y) := -{ section_ := biprod.inr } + is_split_epi (biprod.snd : X ⊞ Y ⟶ Y) := +is_split_epi.mk' { section_ := biprod.inr } @[simp,reassoc] lemma biprod.map_fst {W X Y Z : C} [has_binary_biproduct W X] [has_binary_biproduct Y Z] @@ -1819,7 +1825,7 @@ the cokernel map as its `snd`. We will show in `is_bilimit_binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in fact already a biproduct. -/ @[simps] -def binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono f] +def binary_bicone_of_is_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [is_split_mono f] {c : cokernel_cofork f} (i : is_colimit c) : binary_bicone X c.X := { X := Y, fst := retraction f, @@ -1841,8 +1847,8 @@ def binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono dsimp only [cokernel_cofork_of_cofork_of_π], letI := epi_of_is_colimit_cofork i, apply zero_of_epi_comp c.π, - simp only [sub_comp, comp_sub, category.comp_id, category.assoc, split_mono.id, sub_self, - cofork.is_colimit.π_desc_assoc, cokernel_cofork.π_of_π, split_mono.id_assoc], + simp only [sub_comp, comp_sub, category.comp_id, category.assoc, is_split_mono.id, sub_self, + cofork.is_colimit.π_desc_assoc, cokernel_cofork.π_of_π, is_split_mono.id_assoc], apply sub_eq_zero_of_eq, apply category.id_comp end, @@ -1850,17 +1856,17 @@ def binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono /-- The bicone constructed in `binary_bicone_of_split_mono_of_cokernel` is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories. -/ -def is_bilimit_binary_bicone_of_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [split_mono f] +def is_bilimit_binary_bicone_of_is_split_mono_of_cokernel {X Y : C} {f : X ⟶ Y} [is_split_mono f] {c : cokernel_cofork f} (i : is_colimit c) : - (binary_bicone_of_split_mono_of_cokernel i).is_bilimit := + (binary_bicone_of_is_split_mono_of_cokernel i).is_bilimit := is_binary_bilimit_of_total _ begin - simp only [binary_bicone_of_split_mono_of_cokernel_fst, - binary_bicone_of_split_mono_of_cokernel_inr, binary_bicone_of_split_mono_of_cokernel_snd, + simp only [binary_bicone_of_is_split_mono_of_cokernel_fst, + binary_bicone_of_is_split_mono_of_cokernel_inr, binary_bicone_of_is_split_mono_of_cokernel_snd, split_epi_of_idempotent_of_is_colimit_cofork_section_], - dsimp only [binary_bicone_of_split_mono_of_cokernel_X], + dsimp only [binary_bicone_of_is_split_mono_of_cokernel_X], rw [is_colimit_cofork_of_cokernel_cofork_desc, is_cokernel_epi_comp_desc], - simp only [binary_bicone_of_split_mono_of_cokernel_inl, cofork.is_colimit.π_desc, + simp only [binary_bicone_of_is_split_mono_of_cokernel_inl, cofork.is_colimit.π_desc, cokernel_cofork_of_cofork_π, cofork.π_of_π, add_sub_cancel'_right] end @@ -1923,10 +1929,10 @@ is_binary_bilimit_of_is_colimit _ $ binary_cofan.is_colimit.mk _ /-- Every split epi `f` with a kernel induces a binary bicone with `f` as its `snd` and the kernel map as its `inl`. -We will show in `binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in fact +We will show in `binary_bicone_of_is_split_mono_of_cokernel` that this binary bicone is in fact already a biproduct. -/ @[simps] -def binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f] +def binary_bicone_of_is_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [is_split_epi f] {c : kernel_fork f} (i : is_limit c) : binary_bicone c.X Y := { X := X, fst := @@ -1949,15 +1955,15 @@ def binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f] letI := mono_of_is_limit_fork i, apply zero_of_comp_mono c.ι, simp only [comp_sub, category.comp_id, category.assoc, sub_self, fork.is_limit.lift_ι, - fork.ι_of_ι, split_epi.id_assoc] + fork.ι_of_ι, is_split_epi.id_assoc] end, inr_snd' := by simp } -/-- The bicone constructed in `binary_bicone_of_split_epi_of_kernel` is a bilimit. +/-- The bicone constructed in `binary_bicone_of_is_split_epi_of_kernel` is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories. -/ -def is_bilimit_binary_bicone_of_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [split_epi f] +def is_bilimit_binary_bicone_of_is_split_epi_of_kernel {X Y : C} {f : X ⟶ Y} [is_split_epi f] {c : kernel_fork f} (i : is_limit c) : - (binary_bicone_of_split_epi_of_kernel i).is_bilimit := + (binary_bicone_of_is_split_epi_of_kernel i).is_bilimit := binary_bicone.is_bilimit_of_kernel_inl _ $ i.of_iso_limit $ fork.ext (iso.refl _) (by simp) end diff --git a/src/category_theory/limits/shapes/equalizers.lean b/src/category_theory/limits/shapes/equalizers.lean index 1126c479f3887..0e534c0271773 100644 --- a/src/category_theory/limits/shapes/equalizers.lean +++ b/src/category_theory/limits/shapes/equalizers.lean @@ -911,22 +911,23 @@ lemma has_coequalizers_of_has_colimit_parallel_pair section -- In this section we show that a split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`. -variables {C} [split_mono f] +variables {C} [is_split_mono f] /-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`. -Here we build the cone, and show in `split_mono_equalizes` that it is a limit cone. +Here we build the cone, and show in `is_split_mono_equalizes` that it is a limit cone. -/ @[simps {rhs_md := semireducible}] -def cone_of_split_mono : fork (𝟙 Y) (retraction f ≫ f) := +def cone_of_is_split_mono : fork (𝟙 Y) (retraction f ≫ f) := fork.of_ι f (by simp) -@[simp] lemma cone_of_split_mono_ι : (cone_of_split_mono f).ι = f := rfl +@[simp] lemma cone_of_is_split_mono_ι : (cone_of_is_split_mono f).ι = f := rfl /-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`. -/ -def split_mono_equalizes {X Y : C} (f : X ⟶ Y) [split_mono f] : is_limit (cone_of_split_mono f) := +def is_split_mono_equalizes {X Y : C} (f : X ⟶ Y) [is_split_mono f] : + is_limit (cone_of_is_split_mono f) := fork.is_limit.mk' _ $ λ s, ⟨s.ι ≫ retraction f, by { dsimp, rw [category.assoc, ←s.condition], apply category.comp_id }, @@ -934,7 +935,7 @@ fork.is_limit.mk' _ $ λ s, end -/-- We show that the converse to `split_mono_equalizes` is true: +/-- We show that the converse to `is_split_mono_equalizes` is true: Whenever `f` equalizes `(r ≫ f)` and `(𝟙 Y)`, then `r` is a retraction of `f`. -/ def split_mono_of_equalizer {X Y : C} {f : X ⟶ Y} {r : Y ⟶ X} (hr : f ≫ r ≫ f = f) (h : is_limit (fork.of_ι f (hr.trans (category.comp_id _).symm : f ≫ r ≫ f = f ≫ 𝟙 Y))) : @@ -979,23 +980,23 @@ split_mono_of_idempotent_of_is_limit_fork _ hf (limit.is_limit _) section -- In this section we show that a split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`. -variables {C} [split_epi f] +variables {C} [is_split_epi f] /-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`. -Here we build the cocone, and show in `split_epi_coequalizes` that it is a colimit cocone. +Here we build the cocone, and show in `is_split_epi_coequalizes` that it is a colimit cocone. -/ @[simps {rhs_md := semireducible}] -def cocone_of_split_epi : cofork (𝟙 X) (f ≫ section_ f) := +def cocone_of_is_split_epi : cofork (𝟙 X) (f ≫ section_ f) := cofork.of_π f (by simp) -@[simp] lemma cocone_of_split_epi_π : (cocone_of_split_epi f).π = f := rfl +@[simp] lemma cocone_of_is_split_epi_π : (cocone_of_is_split_epi f).π = f := rfl /-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`. -/ -def split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [split_epi f] : - is_colimit (cocone_of_split_epi f) := +def is_split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [is_split_epi f] : + is_colimit (cocone_of_is_split_epi f) := cofork.is_colimit.mk' _ $ λ s, ⟨section_ f ≫ s.π, by { dsimp, rw [← category.assoc, ← s.condition, category.id_comp] }, @@ -1003,7 +1004,7 @@ cofork.is_colimit.mk' _ $ λ s, end -/-- We show that the converse to `split_epi_equalizes` is true: +/-- We show that the converse to `is_split_epi_equalizes` is true: Whenever `f` coequalizes `(f ≫ s)` and `(𝟙 X)`, then `s` is a section of `f`. -/ def split_epi_of_coequalizer {X Y : C} {f : X ⟶ Y} {s : Y ⟶ X} (hs : f ≫ s ≫ f = f) (h : is_colimit (cofork.of_π f ((category.assoc _ _ _).trans $ diff --git a/src/category_theory/limits/shapes/regular_mono.lean b/src/category_theory/limits/shapes/regular_mono.lean index 080c8d172a6be..1efd3c2609519 100644 --- a/src/category_theory/limits/shapes/regular_mono.lean +++ b/src/category_theory/limits/shapes/regular_mono.lean @@ -13,7 +13,7 @@ import category_theory.limits.shapes.equalizers A regular monomorphism is a morphism that is the equalizer of some parallel pair. We give the constructions -* `split_mono → regular_mono` and +* `is_split_mono → regular_mono` and * `regular_mono → mono` as well as the dual constructions for regular epimorphisms. Additionally, we give the construction * `regular_epi ⟶ strong_epi`. @@ -59,12 +59,12 @@ instance equalizer_regular (g h : X ⟶ Y) [has_limit (parallel_pair g h)] : /-- Every split monomorphism is a regular monomorphism. -/ @[priority 100] -instance regular_mono.of_split_mono (f : X ⟶ Y) [split_mono f] : regular_mono f := +instance regular_mono.of_is_split_mono (f : X ⟶ Y) [is_split_mono f] : regular_mono f := { Z := Y, left := 𝟙 Y, right := retraction f ≫ f, w := by tidy, - is_limit := split_mono_equalizes f } + is_limit := is_split_mono_equalizes f } /-- If `f` is a regular mono, then any map `k : W ⟶ Y` equalizing `regular_mono.left` and `regular_mono.right` induces a morphism `l : W ⟶ X` such that `l ≫ f = k`. -/ @@ -150,7 +150,7 @@ regular_mono_category.regular_mono_of_mono _ instance regular_mono_category_of_split_mono_category [split_mono_category C] : regular_mono_category C := { regular_mono_of_mono := λ _ _ f _, - by { haveI := by exactI split_mono_of_mono f, apply_instance } } + by { haveI := by exactI is_split_mono_of_mono f, apply_instance } } @[priority 100] instance strong_mono_category_of_regular_mono_category [regular_mono_category C] : @@ -183,12 +183,12 @@ instance coequalizer_regular (g h : X ⟶ Y) [has_colimit (parallel_pair g h)] : /-- Every split epimorphism is a regular epimorphism. -/ @[priority 100] -instance regular_epi.of_split_epi (f : X ⟶ Y) [split_epi f] : regular_epi f := +instance regular_epi.of_split_epi (f : X ⟶ Y) [is_split_epi f] : regular_epi f := { W := X, left := 𝟙 X, right := f ≫ section_ f, w := by tidy, - is_colimit := split_epi_coequalizes f } + is_colimit := is_split_epi_coequalizes f } /-- If `f` is a regular epi, then every morphism `k : X ⟶ W` coequalizing `regular_epi.left` and `regular_epi.right` induces `l : Y ⟶ W` such that `f ≫ l = k`. -/ @@ -273,7 +273,7 @@ regular_epi_category.regular_epi_of_epi _ @[priority 100] instance regular_epi_category_of_split_epi_category [split_epi_category C] : regular_epi_category C := -{ regular_epi_of_epi := λ _ _ f _, by { haveI := by exactI split_epi_of_epi f, apply_instance } } +{ regular_epi_of_epi := λ _ _ f _, by { haveI := by exactI is_split_epi_of_epi f, apply_instance } } @[priority 100] instance strong_epi_category_of_regular_epi_category [regular_epi_category C] : diff --git a/src/category_theory/limits/shapes/terminal.lean b/src/category_theory/limits/shapes/terminal.lean index f0cb1eeb9eb1f..3c8cd3fa89c1d 100644 --- a/src/category_theory/limits/shapes/terminal.lean +++ b/src/category_theory/limits/shapes/terminal.lean @@ -116,20 +116,20 @@ t.hom_ext _ _ t.hom_ext _ _ /-- Any morphism from a terminal object is split mono. -/ -def is_terminal.split_mono_from {X Y : C} (t : is_terminal X) (f : X ⟶ Y) : split_mono f := -⟨t.from _, t.hom_ext _ _⟩ +lemma is_terminal.is_split_mono_from {X Y : C} (t : is_terminal X) (f : X ⟶ Y) : + is_split_mono f := is_split_mono.mk' ⟨t.from _, t.hom_ext _ _⟩ /-- Any morphism to an initial object is split epi. -/ -def is_initial.split_epi_to {X Y : C} (t : is_initial X) (f : Y ⟶ X) : split_epi f := -⟨t.to _, t.hom_ext _ _⟩ +lemma is_initial.is_split_epi_to {X Y : C} (t : is_initial X) (f : Y ⟶ X) : + is_split_epi f := is_split_epi.mk' ⟨t.to _, t.hom_ext _ _⟩ /-- Any morphism from a terminal object is mono. -/ lemma is_terminal.mono_from {X Y : C} (t : is_terminal X) (f : X ⟶ Y) : mono f := -by haveI := t.split_mono_from f; apply_instance +by haveI := t.is_split_mono_from f; apply_instance /-- Any morphism to an initial object is epi. -/ lemma is_initial.epi_to {X Y : C} (t : is_initial X) (f : Y ⟶ X) : epi f := -by haveI := t.split_epi_to f; apply_instance +by haveI := t.is_split_epi_to f; apply_instance /-- If `T` and `T'` are terminal, they are isomorphic. -/ @[simps] @@ -284,12 +284,12 @@ initial_is_initial.unique_up_to_iso t terminal_is_terminal.unique_up_to_iso t /-- Any morphism from a terminal object is split mono. -/ -instance terminal.split_mono_from {Y : C} [has_terminal C] (f : ⊤_ C ⟶ Y) : split_mono f := -is_terminal.split_mono_from terminal_is_terminal _ +instance terminal.is_split_mono_from {Y : C} [has_terminal C] (f : ⊤_ C ⟶ Y) : is_split_mono f := +is_terminal.is_split_mono_from terminal_is_terminal _ /-- Any morphism to an initial object is split epi. -/ -instance initial.split_epi_to {Y : C} [has_initial C] (f : Y ⟶ ⊥_ C) : split_epi f := -is_initial.split_epi_to initial_is_initial _ +instance initial.is_split_epi_to {Y : C} [has_initial C] (f : Y ⟶ ⊥_ C) : is_split_epi f := +is_initial.is_split_epi_to initial_is_initial _ /-- An initial object is terminal in the opposite category. -/ def terminal_op_of_initial {X : C} (t : is_initial X) : is_terminal (opposite.op X) := diff --git a/src/category_theory/limits/shapes/zero_morphisms.lean b/src/category_theory/limits/shapes/zero_morphisms.lean index e74ed7ee776ed..00d1e6267f0ed 100644 --- a/src/category_theory/limits/shapes/zero_morphisms.lean +++ b/src/category_theory/limits/shapes/zero_morphisms.lean @@ -160,20 +160,20 @@ by { unfreezingI { subst h, }, apply of_mono_zero X Y, } lemma of_epi_eq_zero {X Y : C} (f : X ⟶ Y) [epi f] (h : f = 0) : is_zero Y := by { unfreezingI { subst h, }, apply of_epi_zero X Y, } -lemma iff_split_mono_eq_zero {X Y : C} (f : X ⟶ Y) [split_mono f] : is_zero X ↔ f = 0 := +lemma iff_is_split_mono_eq_zero {X Y : C} (f : X ⟶ Y) [is_split_mono f] : is_zero X ↔ f = 0 := begin rw iff_id_eq_zero, split, { intro h, rw [←category.id_comp f, h, zero_comp], }, - { intro h, rw [←split_mono.id f], simp [h], }, + { intro h, rw [←is_split_mono.id f], simp [h], }, end -lemma iff_split_epi_eq_zero {X Y : C} (f : X ⟶ Y) [split_epi f] : is_zero Y ↔ f = 0 := +lemma iff_is_split_epi_eq_zero {X Y : C} (f : X ⟶ Y) [is_split_epi f] : is_zero Y ↔ f = 0 := begin rw iff_id_eq_zero, split, { intro h, rw [←category.comp_id f, h, comp_zero], }, - { intro h, rw [←split_epi.id f], simp [h], }, + { intro h, rw [←is_split_epi.id f], simp [h], }, end lemma of_mono {X Y : C} (f : X ⟶ Y) [mono f] (i : is_zero Y) : is_zero X := @@ -519,31 +519,31 @@ by { rw image.eq_fac h, simp } end image /-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/ -instance split_mono_sigma_ι {β : Type u'} [has_zero_morphisms C] (f : β → C) - [has_colimit (discrete.functor f)] (b : β) : split_mono (sigma.ι f b) := +instance is_split_mono_sigma_ι {β : Type u'} [has_zero_morphisms C] (f : β → C) + [has_colimit (discrete.functor f)] (b : β) : is_split_mono (sigma.ι f b) := is_split_mono.mk' { retraction := sigma.desc $ pi.single b (𝟙 _) } /-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/ -instance split_epi_pi_π {β : Type u'} [has_zero_morphisms C] (f : β → C) - [has_limit (discrete.functor f)] (b : β) : split_epi (pi.π f b) := +instance is_split_epi_pi_π {β : Type u'} [has_zero_morphisms C] (f : β → C) + [has_limit (discrete.functor f)] (b : β) : is_split_epi (pi.π f b) := is_split_epi.mk' { section_ := pi.lift $ pi.single b (𝟙 _) } /-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/ -instance split_mono_coprod_inl [has_zero_morphisms C] {X Y : C} [has_colimit (pair X Y)] : - split_mono (coprod.inl : X ⟶ X ⨿ Y) := +instance is_split_mono_coprod_inl [has_zero_morphisms C] {X Y : C} [has_colimit (pair X Y)] : + is_split_mono (coprod.inl : X ⟶ X ⨿ Y) := is_split_mono.mk' { retraction := coprod.desc (𝟙 X) 0, } /-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/ -instance split_mono_coprod_inr [has_zero_morphisms C] {X Y : C} [has_colimit (pair X Y)] : - split_mono (coprod.inr : Y ⟶ X ⨿ Y) := +instance is_split_mono_coprod_inr [has_zero_morphisms C] {X Y : C} [has_colimit (pair X Y)] : + is_split_mono (coprod.inr : Y ⟶ X ⨿ Y) := is_split_mono.mk' { retraction := coprod.desc 0 (𝟙 Y), } /-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/ -instance split_epi_prod_fst [has_zero_morphisms C] {X Y : C} [has_limit (pair X Y)] : - split_epi (prod.fst : X ⨯ Y ⟶ X) := +instance is_split_epi_prod_fst [has_zero_morphisms C] {X Y : C} [has_limit (pair X Y)] : + is_split_epi (prod.fst : X ⨯ Y ⟶ X) := is_split_epi.mk' { section_ := prod.lift (𝟙 X) 0, } /-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/ -instance split_epi_prod_snd [has_zero_morphisms C] {X Y : C} [has_limit (pair X Y)] : - split_epi (prod.snd : X ⨯ Y ⟶ Y) := +instance is_split_epi_prod_snd [has_zero_morphisms C] {X Y : C} [has_limit (pair X Y)] : + is_split_epi (prod.snd : X ⨯ Y ⟶ Y) := is_split_epi.mk' { section_ := prod.lift 0 (𝟙 Y), } end category_theory.limits diff --git a/src/category_theory/simple.lean b/src/category_theory/simple.lean index 544a488f70555..c7f2433aeaccd 100644 --- a/src/category_theory/simple.lean +++ b/src/category_theory/simple.lean @@ -190,8 +190,9 @@ begin rw [biprod.is_iso_inl_iff_id_eq_fst_comp_inl, ←biprod.total, add_right_eq_self], split, { intro h, replace h := h =≫ biprod.snd, - simpa [←is_zero.iff_split_epi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h, }, - { intro h, rw is_zero.iff_split_epi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y) at h, rw [h, zero_comp], }, + simpa [←is_zero.iff_is_split_epi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h, }, + { intro h, rw is_zero.iff_is_split_epi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y) at h, + rw [h, zero_comp], }, end /-- Any simple object in a preadditive category is indecomposable. -/ @@ -199,7 +200,7 @@ lemma indecomposable_of_simple (X : C) [simple X] : indecomposable X := ⟨simple.not_is_zero X, λ Y Z i, begin refine or_iff_not_imp_left.mpr (λ h, _), - rw is_zero.iff_split_mono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z) at h, + rw is_zero.iff_is_split_mono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z) at h, change biprod.inl ≠ 0 at h, rw ←(simple.mono_is_iso_iff_nonzero biprod.inl) at h, { rwa biprod.is_iso_inl_iff_is_zero at h, }, diff --git a/src/category_theory/sites/sheaf_of_types.lean b/src/category_theory/sites/sheaf_of_types.lean index 5a9368fd1a502..fd0b2296cd3ac 100644 --- a/src/category_theory/sites/sheaf_of_types.lean +++ b/src/category_theory/sites/sheaf_of_types.lean @@ -663,7 +663,7 @@ Every presheaf is a sheaf for the maximal sieve. lemma is_sheaf_for_top_sieve (P : Cᵒᵖ ⥤ Type w) : is_sheaf_for P ((⊤ : sieve X) : presieve X) := begin - rw ← generate_of_singleton_split_epi (𝟙 X), + rw ← generate_of_singleton_is_split_epi (𝟙 X), rw ← is_sheaf_for_iff_generate, apply is_sheaf_for_singleton_iso, end diff --git a/src/category_theory/sites/sieves.lean b/src/category_theory/sites/sieves.lean index f0453fb0c5c4d..fcb14e3bb6273 100644 --- a/src/category_theory/sites/sieves.lean +++ b/src/category_theory/sites/sieves.lean @@ -357,7 +357,7 @@ lemma id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ := λ h, h.symm ▸ trivial⟩ /-- If an arrow set contains a split epi, it generates the maximal sieve. -/ -lemma generate_of_contains_split_epi {R : presieve X} (f : Y ⟶ X) [split_epi f] +lemma generate_of_contains_is_split_epi {R : presieve X} (f : Y ⟶ X) [is_split_epi f] (hf : R f) : generate R = ⊤ := begin rw ← id_mem_iff_eq_top, @@ -365,13 +365,13 @@ begin end @[simp] -lemma generate_of_singleton_split_epi (f : Y ⟶ X) [split_epi f] : +lemma generate_of_singleton_is_split_epi (f : Y ⟶ X) [is_split_epi f] : generate (presieve.singleton f) = ⊤ := -generate_of_contains_split_epi f (presieve.singleton_self _) +generate_of_contains_is_split_epi f (presieve.singleton_self _) @[simp] lemma generate_top : generate (⊤ : presieve X) = ⊤ := -generate_of_contains_split_epi (𝟙 _) ⟨⟩ +generate_of_contains_is_split_epi (𝟙 _) ⟨⟩ /-- Given a morphism `h : Y ⟶ X`, send a sieve S on X to a sieve on Y as the inverse image of S with `_ ≫ h`. @@ -470,7 +470,7 @@ begin end /-- If `f` is a split epi, the pushforward-pullback adjunction on sieves is reflective. -/ -def galois_insertion_of_split_epi (f : Y ⟶ X) [split_epi f] : +def galois_insertion_of_is_split_epi (f : Y ⟶ X) [is_split_epi f] : galois_insertion (sieve.pushforward f) (sieve.pullback f) := begin apply (galois_connection f).to_galois_insertion, @@ -599,7 +599,7 @@ lemma functor_pullback_inter (S R : sieve (F.obj X)) : (⊤ : sieve X).functor_pushforward F = ⊤ := begin refine (generate_sieve _).symm.trans _, - apply generate_of_contains_split_epi (𝟙 (F.obj X)), + apply generate_of_contains_is_split_epi (𝟙 (F.obj X)), refine ⟨X, 𝟙 _, 𝟙 _, trivial, by simp⟩ end diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean index e1074994e2618..41c59d98a3a8b 100644 --- a/src/category_theory/types.lean +++ b/src/category_theory/types.lean @@ -278,8 +278,8 @@ iff.intro (λ i, (by exactI as_iso f : X ≅ Y).to_equiv.bijective) (λ b, is_iso.of_iso (equiv.of_bijective f b).to_iso) -noncomputable instance : split_epi_category (Type u) := -{ split_epi_of_epi := λ X Y f hf, +instance : split_epi_category (Type u) := +{ is_split_epi_of_epi := λ X Y f hf, is_split_epi.mk' { section_ := function.surj_inv $ (epi_iff_surjective f).1 hf, id' := funext $ function.right_inverse_surj_inv $ (epi_iff_surjective f).1 hf } }