From b7b1061ba7483b4fa01cf74035ce107c2c8bd638 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Fri, 14 Jun 2024 14:57:49 +0200 Subject: [PATCH] ... --- LeanCondensed/Projects/AB.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/LeanCondensed/Projects/AB.lean b/LeanCondensed/Projects/AB.lean index 059e4f5..4121c57 100644 --- a/LeanCondensed/Projects/AB.lean +++ b/LeanCondensed/Projects/AB.lean @@ -36,7 +36,7 @@ lemma forall_exact_iff_functorEquivalence_exact (F : I ⥤ ShortComplex A) : ( class HasExactLimitsOfShape : Prop where hasLimitsOfShape : HasLimitsOfShape I A := by infer_instance - exact_limit : ∀ (F : I ⥤ ShortComplex A), (∀ i, (F.obj i).ShortExact) → (limit F).ShortExact + exact_limit (F : I ⥤ ShortComplex A) : (∀ i, (F.obj i).ShortExact) → (limit F).ShortExact attribute [instance] HasExactLimitsOfShape.hasLimitsOfShape @@ -57,7 +57,7 @@ lemma hasExactLimitsOfShape_iff_limitCone_shortExact [HasLimitsOfShape I A] : class HasExactColimitsOfShape : Prop where hasColimitsOfShape : HasColimitsOfShape I A := by infer_instance - exact_colimit : ∀ (F : I ⥤ ShortComplex A), (∀ i, (F.obj i).ShortExact) → (colimit F).ShortExact + exact_colimit (F : I ⥤ ShortComplex A) : (∀ i, (F.obj i).ShortExact) → (colimit F).ShortExact attribute [instance] HasExactColimitsOfShape.hasColimitsOfShape @@ -71,7 +71,6 @@ lemma hasExactColimitsOfShape_iff_colim_leftExact [HasLimitsOfShape I A] : HasExactLimitsOfShape I A ↔ Nonempty (PreservesFiniteColimits (lim : (I ⥤ A) ⥤ A)) := ⟨fun _ ↦ ⟨inferInstance⟩, fun ⟨_⟩ ↦ inferInstance⟩ --- NR: I think the bracketing on this one was off. lemma hasExactColimitsOfShape_iff_colimitCocone_shortExact [HasColimitsOfShape I A] : HasExactColimitsOfShape I A ↔ ∀ (F : I ⥤ ShortComplex A), ((∀ i, (F.obj i).ShortExact) → (colimitCocone F).pt.ShortExact) := @@ -100,7 +99,7 @@ end section variable (A : Type*) [Category A] [Abelian A] -variable (I : Type*) [Category I] -- +variable (I : Type*) [Category I] lemma mono_of_mono [HasLimitsOfShape I A] (F : I ⥤ ShortComplex A) (h : ∀ i, Mono (F.obj i).f) : Mono (ShortComplex.limitCone F).pt.f := by @@ -115,7 +114,6 @@ lemma left_exact_of_left_exact [HasLimitsOfShape I A] (F : I ⥤ ShortComplex A) Mono (ShortComplex.limitCone F).pt.f ∧ (ShortComplex.limitCone F).pt.Exact := by sorry --- NR: Made this one up, think it should be what we want. lemma right_exact_of_right_exact [HasColimitsOfShape I A] (F : I ⥤ ShortComplex A) (h : ∀ i, Epi (F.obj i).g ∧ (F.obj i).Exact) : Epi (ShortComplex.colimitCocone F).pt.g ∧ (ShortComplex.colimitCocone F).pt.Exact := by