Skip to content

Commit da8281b

Browse files
chrisflavchrisflav
committed
some cleanup
1 parent 84da266 commit da8281b

6 files changed

Lines changed: 90 additions & 143 deletions

File tree

‎Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,24 @@ lemma pushforwardPushforwardAdj_counit_app_val_app (M U x) :
256256
((pushforwardPushforwardAdj adj φ ψ H₁ H₂).counit.app M).val.app U x =
257257
M.val.map (adj.unit.app U.unop).op x := rfl
258258

259+
set_option backward.defeqAttrib.useBackward true in
260+
instance isLeftAdjoint_pushforward_of_isIso [F.IsCocontinuous J K] [IsIso φ] [F.IsLeftAdjoint] :
261+
(pushforward.{u} φ).IsLeftAdjoint := by
262+
let adj := Adjunction.ofIsLeftAdjoint F
263+
let shAdj := adj.sheafPushforwardContinuous (E := RingCat.{u}) J K
264+
let ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat.{u} K J).obj S :=
265+
shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous _ _ _).map (inv φ)
266+
refine (SheafOfModules.pushforwardPushforwardAdj adj φ ψ ?_ ?_).isLeftAdjoint
267+
· ext U : 2
268+
simp [ψ, shAdj]
269+
· ext U : 2
270+
have := (inv φ).hom.naturality
271+
dsimp at this
272+
simp only [ObjectProperty.hom_inv, NatIso.isIso_inv_app, sheafPushforwardContinuous_obj_obj_obj,
273+
IsIso.eq_inv_comp] at this
274+
simp [ψ, shAdj, ← this, ← Functor.map_comp_assoc, ← op_comp]
275+
276+
259277
noncomputable section
260278

261279
open CategoryTheory Limits

‎Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean‎

Lines changed: 49 additions & 138 deletions
Original file line numberDiff line numberDiff line change
@@ -287,168 +287,81 @@ instance (M : SheafOfModules.{u} R) [M.IsFinitePresentation] :
287287

288288
section map
289289

290-
set_option backward.isDefEq.respectTransparency false
291-
292-
variable {J : GrothendieckTopology C}
293-
{R : Sheaf J RingCat} [HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat]
294-
[J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)] {C' : Type u₂} [Category.{v₂, u₂} C']
295-
{J' : GrothendieckTopology C'} {S : Sheaf J' RingCat.{u}} [HasSheafify J' AddCommGrpCat.{u}]
296-
[J'.WEqualsLocallyBijective AddCommGrpCat.{u}]
297-
[J'.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
298-
{M : SheafOfModules.{u} R}
299-
(P : M.Presentation) (F : SheafOfModules.{u} R ⥤ SheafOfModules.{u} S)
300-
[PreservesColimitsOfSize.{u, u} F]
301-
(η : F.obj (unit R) ≅ unit S)
302-
[∀ (X : C), (J.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
303-
[∀ (X : C), HasSheafify (J.over X) AddCommGrpCat]
304-
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
305-
[∀ (X : C'), (J'.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
306-
[∀ (X : C'), HasSheafify (J'.over X) AddCommGrpCat]
307-
[∀ (X : C'), (J'.over X).WEqualsLocallyBijective AddCommGrpCat]
308-
309-
noncomputable
310-
def QuasicoherentData.pushforward
311-
(G : C' ⥤ C) [G.IsContinuous J' J] [G.IsCocontinuous J' J]
312-
(φ : S ⟶ (G.sheafPushforwardContinuous RingCat.{u} J' J).obj R)
313-
[∀ (X : C') (Y : C) (f : G.obj X ⟶ Y),
314-
(Over.post G ⋙ Over.map f).IsContinuous (J'.over X) (J.over Y)]
315-
(h : ∀ (X : C') (Y : C) (f : G.obj X ⟶ Y),
290+
variable {D : Type u₂} [Category.{v₂, u₂} D] {K : GrothendieckTopology D}
291+
{S : Sheaf K RingCat.{u}} [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
292+
[∀ (X : D), (K.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
293+
294+
variable [J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
295+
[K.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
296+
[∀ (X : C), HasSheafify (J.over X) AddCommGrpCat.{u}]
297+
[∀ (X : D), HasSheafify (K.over X) AddCommGrpCat.{u}]
298+
299+
instance {G : C ⥤ D} (X : C) (Y : D) (f : G.obj X ⟶ Y)
300+
[(Over.post G).IsContinuous (J.over X) (K.over _)] :
301+
(Over.post G ⋙ Over.map f).IsContinuous (J.over X) (K.over Y) :=
302+
Functor.isContinuous_comp _ _ _ (K.over _) _
303+
304+
variable (G : D ⥤ C) [G.IsContinuous K J] [G.IsCocontinuous K J]
305+
(φ : S ⟶ (G.sheafPushforwardContinuous RingCat.{u} K J).obj R)
306+
307+
/-- The pushforward of `SheafOfModules.QuasicoherentData` along a continuous
308+
and cocontinuous functor. -/
309+
-- TODO: Remove the continuous assumption on `Over.post` here and below.
310+
@[simps I X]
311+
noncomputable def QuasicoherentData.pushforward (η : (pushforward φ).obj (unit R) ≅ unit S)
312+
[∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over _)]
313+
(h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
316314
PreservesColimitsOfSize.{u, u} <|
317315
pushforward.{u} (R := (R.over Y)) (F := Over.post (X := X) G ⋙ Over.map f)
318-
(((Over.forget X).sheafPushforwardContinuous RingCat.{u} (J'.over X) J').map φ))
319-
(η : (pushforward φ).obj (unit R) ≅ unit S)
316+
(((Over.forget X).sheafPushforwardContinuous RingCat.{u} (K.over X) K).map φ))
320317
{M : SheafOfModules.{u} R} (P : M.QuasicoherentData) :
321318
QuasicoherentData ((pushforward φ).obj M) where
322-
I := Σ (X : C') (i : P.I), G.obj X ⟶ P.X i
319+
I := Σ (X : D) (i : P.I), G.obj X ⟶ P.X i
323320
X i := i.1
324-
coversTop := by
325-
intro Y
326-
refine J'.superset_covering ?_ <| G.cover_lift J' _ (P.coversTop (G.obj Y))
321+
coversTop Y := by
322+
refine K.superset_covering ?_ <| G.cover_lift K _ (P.coversTop (G.obj Y))
327323
intro Z g ⟨i, ⟨v⟩⟩
328324
exact ⟨⟨Z, i, v⟩, ⟨𝟙 _⟩⟩
329325
presentation i := by
330326
letI overS : SheafOfModules.{u} S ⥤ SheafOfModules.{u} (S.over i.1) :=
331327
SheafOfModules.pushforward (𝟙 _)
332328
letI G' := Over.post (X := i.1) G ⋙ Over.map i.2.2
333329
letI ψ : S.over i.1 ⟶
334-
(G'.sheafPushforwardContinuous RingCat.{u} (J'.over i.1) (J.over (P.X i.2.1))).obj
330+
(G'.sheafPushforwardContinuous RingCat.{u} (K.over i.1) (J.over (P.X i.2.1))).obj
335331
(R.over (P.X i.2.1)) :=
336-
((Over.forget i.1).sheafPushforwardContinuous RingCat.{u} (J'.over i.1) J').map φ
332+
((Over.forget i.1).sheafPushforwardContinuous RingCat.{u} (K.over i.1) K).map φ
337333
letI e : (SheafOfModules.pushforward ψ).obj (unit (R.over (P.X i.snd.fst))) ≅
338334
unit (S.over i.fst) := overS.mapIso η
339335
haveI : PreservesColimitsOfSize.{u, u, _} (SheafOfModules.pushforward ψ) := h _ _ _
340336
exact (P.presentation i.2.1).map (SheafOfModules.pushforward ψ) e.symm
341337

342-
omit [HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective
343-
AddCommGrpCat] [HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] in
344-
lemma isQuasicoherent_pushforward
345-
(G : C' ⥤ C) [G.IsContinuous J' J] [G.IsCocontinuous J' J]
346-
(φ : S ⟶ (G.sheafPushforwardContinuous RingCat.{u} J' J).obj R)
347-
[∀ (X : C') (Y : C) (f : G.obj X ⟶ Y),
348-
(Over.post G ⋙ Over.map f).IsContinuous (J'.over X) (J.over Y)]
349-
(h : ∀ (X : C') (Y : C) (f : G.obj X ⟶ Y),
338+
lemma isQuasicoherent_pushforward (η : (pushforward φ).obj (unit R) ≅ unit S)
339+
[∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over _)]
340+
(h : ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
350341
PreservesColimitsOfSize.{u, u} <|
351342
pushforward.{u} (R := (R.over Y)) (F := Over.post (X := X) G ⋙ Over.map f)
352-
(((Over.forget X).sheafPushforwardContinuous RingCat.{u} (J'.over X) J').map φ))
353-
(η : (pushforward φ).obj (unit R) ≅ unit S)
343+
(((Over.forget X).sheafPushforwardContinuous RingCat.{u} (K.over X) K).map φ))
354344
{M : SheafOfModules.{u} R} [IsQuasicoherent M] :
355345
IsQuasicoherent ((pushforward φ).obj M) :=
356-
IsQuasicoherent.nonempty_quasicoherentData.some.pushforward G φ h η |>.isQuasicoherent
357-
358-
lemma _root_.CategoryTheory.PreOneHypercover.sieve₀_map
359-
{C D : Type*} [Category* C] [Category* D] (F : C ⥤ D) {S : C}
360-
(E : PreOneHypercover.{w} S) :
361-
(E.map F).sieve₀ = Sieve.functorPushforward _ E.sieve₀ := by
362-
rw [PreZeroHypercover.sieve₀, Sieve.ofArrows, ← PreZeroHypercover.presieve₀,
363-
PreOneHypercover.map_toPreZeroHypercover, PreZeroHypercover.presieve₀_map,
364-
Sieve.generate_map_eq_functorPushforward]
365-
366-
lemma coverPreserving_of_coverPreserving_comp {C D E : Type*} [Category* C] [Category* D]
367-
[Category* E] (F : C ⥤ D) (G : D ⥤ E) (J : GrothendieckTopology C) (K : GrothendieckTopology D)
368-
(T : GrothendieckTopology E) (h : CoverPreserving J T (F ⋙ G)) [G.IsCocontinuous K T]
369-
[G.Full] [G.Faithful] :
370-
CoverPreserving J K F where
371-
cover_preserve {U} S hS := by
372-
refine K.superset_covering ?_ (G.cover_lift K _ (h.cover_preserve hS))
373-
rw [Sieve.functorPushforward_comp, Sieve.functorPullback_functorPushforward_eq G]
374-
375-
lemma _root_.CategoryTheory.coverPreserving_of_preservesOneHypercovers {C : Type u₁} {D : Type*}
376-
[Category.{v₁} C] [Category* D] (F : C ⥤ D) (J : GrothendieckTopology C)
377-
(K : GrothendieckTopology D) [Functor.PreservesOneHypercovers.{max u₁ v₁} F J K] :
378-
CoverPreserving J K F where
379-
cover_preserve {U} S hS := by
380-
let E := GrothendieckTopology.Cover.oneHypercover ⟨_, hS⟩
381-
simpa [CategoryTheory.PreZeroHypercover.sieve₀_map, E] using (E.map F K).mem₀
382-
383-
instance {C : Type*} [Category* C] {A : Type*} [Category* A]
384-
(J : GrothendieckTopology C) {F G : Sheaf J A} (f : F ⟶ G) [IsIso f] :
385-
IsIso f.hom := by
386-
refine ⟨(inv f).hom, ?_, ?_⟩
387-
· simp [IsIso.hom_inv_id]
388-
· simp [IsIso.inv_hom_id]
389-
390-
set_option backward.defeqAttrib.useBackward true in
391-
omit
392-
[HasSheafify J AddCommGrpCat]
393-
[J.WEqualsLocallyBijective AddCommGrpCat]
394-
[J.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
395-
[HasSheafify J' AddCommGrpCat]
396-
[J'.WEqualsLocallyBijective AddCommGrpCat]
397-
[J'.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
398-
[∀ (X : C), (J.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
399-
[∀ (X : C), HasSheafify (J.over X) AddCommGrpCat]
400-
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
401-
[∀ (X : C'), (J'.over X).HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
402-
[∀ (X : C'), HasSheafify (J'.over X) AddCommGrpCat]
403-
[∀ (X : C'), (J'.over X).WEqualsLocallyBijective AddCommGrpCat] in
404-
lemma isLeftAdjoint_pushforward_of_isIso (G : C' ⥤ C) [G.IsContinuous J' J] [G.IsCocontinuous J' J]
405-
(φ : S ⟶ (G.sheafPushforwardContinuous RingCat.{u} J' J).obj R) [IsIso φ]
406-
[G.IsLeftAdjoint] :
407-
(pushforward.{u} φ).IsLeftAdjoint := by
408-
let adj := Adjunction.ofIsLeftAdjoint G
409-
let shAdj := adj.sheafPushforwardContinuous (E := RingCat.{u}) J' J
410-
let ψ : R ⟶ (G.rightAdjoint.sheafPushforwardContinuous RingCat.{u} J J').obj S :=
411-
shAdj.unit.app R ≫ (G.rightAdjoint.sheafPushforwardContinuous _ _ _).map (inv φ)
412-
let adj := by
413-
refine SheafOfModules.pushforwardPushforwardAdj adj φ ψ ?_ ?_
414-
· ext U : 2
415-
simp [ψ, shAdj]
416-
· ext U : 2
417-
have := (inv φ).hom.naturality
418-
simp only [Functor.sheafPushforwardContinuous_obj_obj_obj,
419-
Functor.sheafPushforwardContinuous_obj_obj_map, ObjectProperty.hom_inv,
420-
NatIso.isIso_inv_app, IsIso.eq_inv_comp] at this
421-
simp [ψ, shAdj, ← this, ← Functor.map_comp_assoc, ← op_comp]
422-
exact adj.isLeftAdjoint
423-
424-
instance {C : Type*} [Category* C] [HasPullbacks C] {X Y : C} (f : X ⟶ Y) :
425-
(Over.map f).IsLeftAdjoint :=
426-
(Over.mapPullbackAdj f).isLeftAdjoint
346+
IsQuasicoherent.nonempty_quasicoherentData.some.pushforward G φ η h |>.isQuasicoherent
427347

428348
set_option backward.isDefEq.respectTransparency false in
429-
omit [HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat]
430-
[HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] in
431-
lemma isQuasicoherent_pushforward_of_isLeftAdjoint (G : C' ⥤ C) [G.IsLeftAdjoint]
432-
[G.IsContinuous J' J] [G.IsCocontinuous J' J]
433-
(φ : S ⟶ (G.sheafPushforwardContinuous RingCat.{u} J' J).obj R) [IsIso φ]
434-
[∀ X, Functor.IsContinuous (Over.post (X := X) G) (J'.over _) (J.over _)]
435-
[HasPullbacks C] [HasPullbacks C']
436-
(η : (pushforward φ).obj (unit R) ≅ unit S)
349+
lemma isQuasicoherent_pushforward_of_isLeftAdjoint (η : (pushforward φ).obj (unit R) ≅ unit S)
350+
[G.IsLeftAdjoint] [IsIso φ]
351+
[∀ X, Functor.IsContinuous (Over.post (X := X) G) (K.over _) (J.over _)]
352+
[HasPullbacks C] [HasPullbacks D]
437353
{M : SheafOfModules.{u} R} [IsQuasicoherent M] :
438354
IsQuasicoherent ((pushforward φ).obj M) := by
439-
convert isQuasicoherent_pushforward G φ _ η
440-
· intro X Y f
441-
apply Functor.isContinuous_comp _ _ _ (J.over _) _
442-
· intro X Y f
443-
let G' := Over.post (X := X) G ⋙ Over.map f
444-
have : G'.IsContinuous (J'.over X) (J.over Y) := Functor.isContinuous_comp _ _ _ (J.over _) _
445-
have : G'.IsCocontinuous (J'.over X) (J.over Y) := isCocontinuous_comp _ _ _ (J.over _)
446-
let a : S.over X ⟶
447-
(G'.sheafPushforwardContinuous RingCat.{u} (J'.over X) (J.over Y)).obj (R.over Y) :=
448-
((Over.forget X).sheafPushforwardContinuous RingCat.{u} (J'.over X) J').map φ
449-
have : (pushforward.{u} a).IsLeftAdjoint := isLeftAdjoint_pushforward_of_isIso _ _
450-
infer_instance
451-
· infer_instance
355+
apply +allowSynthFailures isQuasicoherent_pushforward G φ η _
356+
intro X Y f
357+
let G' := Over.post (X := X) G ⋙ Over.map f
358+
have : G'.IsContinuous (K.over X) (J.over Y) := Functor.isContinuous_comp _ _ _ (J.over _) _
359+
have : G'.IsCocontinuous (K.over X) (J.over Y) := isCocontinuous_comp _ _ _ (J.over _)
360+
let a : S.over X ⟶
361+
(G'.sheafPushforwardContinuous RingCat.{u} (K.over X) (J.over Y)).obj (R.over Y) :=
362+
((Over.forget X).sheafPushforwardContinuous RingCat.{u} (K.over X) K).map φ
363+
have : (pushforward.{u} a).IsLeftAdjoint := isLeftAdjoint_pushforward_of_isIso a
364+
infer_instance
452365

453366
end map
454367

@@ -545,8 +458,6 @@ lemma IsQuasicoherent.of_coversTop {R : Sheaf J RingCat.{u}}
545458
(QuasicoherentData.bind M X hX fun _ ↦
546459
IsQuasicoherent.nonempty_quasicoherentData.some).isQuasicoherent
547460

548-
set_option backward.isDefEq.respectTransparency false
549-
550461
set_option backward.isDefEq.respectTransparency false in
551462
lemma isQuasicoherent_over [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
552463
[HasPullbacks C] [HasBinaryProducts C] (M : SheafOfModules.{u} R) (X : C) [IsQuasicoherent M] :

‎Mathlib/AlgebraicGeometry/Modules/Tilde.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -661,11 +661,7 @@ lemma Scheme.Modules.isQuasicoherent_restrictFunctor {X Y : Scheme.{u}} (f : X
661661
have hα : IsIso α := NatIso.isIso_of_isIso_app _
662662
dsimp [restrictFunctor]
663663
convert SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint.{u}
664-
(J := Opens.grothendieckTopology _) (J' := Opens.grothendieckTopology _) f.opensFunctor _ _
665-
· convert isIso_of_reflects_iso _ (ObjectProperty.ι _)
666-
· dsimp
667-
infer_instance
668-
· infer_instance
664+
(J := Opens.grothendieckTopology _) (K := Opens.grothendieckTopology _) f.opensFunctor _ _
669665
· refine (SheafOfModules.fullyFaithfulForget _).preimageIso ?_
670666
refine PresheafOfModules.isoMk ?_ ?_
671667
· intro U
@@ -674,6 +670,10 @@ lemma Scheme.Modules.isQuasicoherent_restrictFunctor {X Y : Scheme.{u}} (f : X
674670
· intro U V g
675671
ext x
676672
exact congr($(f.appIso_hom_naturality _).hom x)
673+
· convert isIso_of_reflects_iso _ (ObjectProperty.ι _)
674+
· dsimp
675+
infer_instance
676+
· infer_instance
677677
· infer_instance
678678

679679
end AlgebraicGeometry

‎Mathlib/CategoryTheory/Comma/Over/Pullback.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,12 @@ def mapPullbackAdj {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] :
8787
· simp
8888
· simpa using (Over.w v).symm } }
8989

90+
instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : (Over.map f).IsLeftAdjoint :=
91+
(Over.mapPullbackAdj f).isLeftAdjoint
92+
93+
instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : (Over.pullback f).IsRightAdjoint :=
94+
(Over.mapPullbackAdj f).isRightAdjoint
95+
9096
set_option backward.isDefEq.respectTransparency false in
9197
/-- The pullback along an epi that's preserved under pullbacks is faithful.
9298

‎Mathlib/CategoryTheory/Sites/Continuous.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ lemma map_id : E.map (𝟭 _) = E :=
8080
lemma map_comp {D' : Type*} [Category* D'] (G : D ⥤ D') : E.map (F ⋙ G) = (E.map F).map G :=
8181
rfl
8282

83+
lemma sieve₀_map : (E.map F).sieve₀ = Sieve.functorPushforward _ E.sieve₀ := by
84+
rw [PreZeroHypercover.sieve₀, Sieve.ofArrows, ← PreZeroHypercover.presieve₀,
85+
PreOneHypercover.map_toPreZeroHypercover, PreZeroHypercover.presieve₀_map,
86+
Sieve.generate_map_eq_functorPushforward]
87+
8388
/-- If `F : C ⥤ D`, `P : Dᵒᵖ ⥤ A` and `E` is a 1-pre-hypercover of an object of `X`,
8489
then `(E.map F).multifork P` is a limit iff `E.multifork (F.op ⋙ P)` is a limit. -/
8590
def isLimitMapMultiforkEquiv {A : Type u} [Category.{t} A] (P : Dᵒᵖ ⥤ A) :

‎Mathlib/CategoryTheory/Sites/CoverLifting.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,13 @@ lemma Functor.IsCocontinuous.iff_of_iso {F G : C ⥤ D} (e : F ≅ G) :
102102
F.IsCocontinuous J K ↔ G.IsCocontinuous J K :=
103103
⟨fun _ ↦ .of_iso e, fun _ ↦ .of_iso e.symm⟩
104104

105+
lemma CoverPreserving.of_comp_of_isCocontinuous {F : C ⥤ D} (G : D ⥤ E)
106+
(h : CoverPreserving J L (F ⋙ G)) [G.IsCocontinuous K L] [G.Full] [G.Faithful] :
107+
CoverPreserving J K F where
108+
cover_preserve {U} S hS := by
109+
refine K.superset_covering ?_ (G.cover_lift K _ (h.cover_preserve hS))
110+
rw [Sieve.functorPushforward_comp, Sieve.functorPullback_functorPushforward_eq G]
111+
105112
section
106113

107114
variable {F : C ⥤ D} {G : D ⥤ C}

0 commit comments

Comments
 (0)