Skip to content

Commit 028b72c

Browse files
joelrioujoelriou
committed
feat(AlgebraicGeometry): points of the small étale site (#35136)
The main definition in this PR is `Scheme.pointSmallEtale`. Given a morphism `Spec (.of Ω) ⟶ S` where `Ω` is a separably closed field, we define the corresponding point of the small étale site of `S`. We show that these points form a conservative family. (This PR also removes the definition `Scheme.geometricFiber` which was not correct.) Co-authored-by: Christian Merten
1 parent ec6e08b commit 028b72c

12 files changed

Lines changed: 302 additions & 7 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1458,6 +1458,7 @@ public import Mathlib.AlgebraicGeometry.Sites.BigZariski
14581458
public import Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
14591459
public import Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
14601460
public import Mathlib.AlgebraicGeometry.Sites.Etale
1461+
public import Mathlib.AlgebraicGeometry.Sites.EtalePoint
14611462
public import Mathlib.AlgebraicGeometry.Sites.Fpqc
14621463
public import Mathlib.AlgebraicGeometry.Sites.MorphismProperty
14631464
public import Mathlib.AlgebraicGeometry.Sites.Pretopology

‎Mathlib/AlgebraicGeometry/Fiber.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,11 @@ def Scheme.Hom.fiberToSpecResidueField (f : X ⟶ Y) (y : Y) :
4747
f.fiber y ⟶ Spec (Y.residueField y) :=
4848
pullback.snd _ _
4949

50+
@[reassoc]
51+
lemma Scheme.Hom.fiber_fac (f : X ⟶ Y) (y : Y) :
52+
f.fiberι y ≫ f = f.fiberToSpecResidueField y ≫ Y.fromSpecResidueField y :=
53+
pullback.condition
54+
5055
/-- The fiber of `f` at `y` is naturally a `κ(y)`-scheme. -/
5156
@[reducible] def Scheme.Hom.fiberOverSpecResidueField
5257
(f : X ⟶ Y) (y : Y) : (f.fiber y).Over (Spec (Y.residueField y)) where

‎Mathlib/AlgebraicGeometry/Morphisms/Etale.lean‎

Lines changed: 47 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -149,21 +149,65 @@ namespace Scheme
149149

150150
/-- The category `Etale X` is the category of schemes étale over `X`. -/
151151
protected def Etale (X : Scheme.{u}) : Type _ := MorphismProperty.Over @Etale ⊤ X
152-
deriving Category, HasPullbacks
152+
deriving Category, HasPullbacks, HasFiniteLimits
153153

154154
variable (X : Scheme.{u})
155155

156-
instance (Y : X.Etale) : Etale Y.hom := Y.prop
156+
set_option backward.defeqAttrib.useBackward true in
157+
instance (Y : X.Etale) : dsimp% Etale Y.hom := Y.prop
158+
159+
instance {X : Scheme.{u}} {Z Y : X.Etale} (f : Z ⟶ Y) : Etale f.left := by
160+
have : Etale (f.left ≫ Y.hom) := by rw [CategoryTheory.Over.w]; infer_instance
161+
exact Etale.of_comp f.left Y.hom
157162

158163
/-- The forgetful functor from schemes étale over `X` to schemes over `X`. -/
159164
def Etale.forget : X.Etale ⥤ Over X :=
160165
MorphismProperty.Over.forget @Etale ⊤ X
161-
deriving Functor.Full, Functor.Faithful
162166

163167
/-- The forgetful functor from schemes étale over `X` to schemes over `X` is fully faithful. -/
164168
def Etale.forgetFullyFaithful : (Etale.forget X).FullyFaithful :=
165169
MorphismProperty.Comma.forgetFullyFaithful _ _ _
166170

171+
-- Note: using `deriving Functor.Full/Faithful` in the declaration of `Etale.forget`
172+
-- would "succeed", but it seems it would fail to create the next two instances
173+
instance : (Etale.forget X).Full :=
174+
(Etale.forgetFullyFaithful X).full
175+
176+
instance : (Etale.forget X).Faithful :=
177+
(Etale.forgetFullyFaithful X).faithful
178+
179+
variable {X} in
180+
/-- Constructor for objects in the étale site of a scheme `X`: it takes
181+
an étale morphism `f : Y ⟶ X` as an input. -/
182+
abbrev Etale.mk {Y : Scheme.{u}} (f : Y ⟶ X) [Etale f] : X.Etale :=
183+
MorphismProperty.Over.mk _ f inferInstance
184+
185+
variable {X} in
186+
@[simp]
187+
lemma Etale.forget_mk {Y : Scheme.{u}} (f : Y ⟶ X) [Etale f] :
188+
(Etale.forget X).obj (.mk f) = Over.mk f := rfl
189+
190+
@[simp]
191+
lemma Etale.forget_obj_left (Y : X.Etale) :
192+
((Etale.forget X).obj Y).left = Y.left := rfl
193+
194+
@[simp]
195+
lemma Etale.forget_obj_hom (Y : X.Etale) :
196+
((Etale.forget X).obj Y).hom = Y.hom := rfl
197+
198+
instance (Y : X.Etale) : Etale (Y.left ↘ X) := Y.prop
199+
200+
/-- Induction principle for the objects of the small étale site of a scheme. -/
201+
@[elab_as_elim, cases_eliminator, induction_eliminator]
202+
def Etale.rec {motive : X.Etale → Sort*}
203+
(mk : ∀ (Y : Scheme.{u}) (f : Y ⟶ X) (_ : Etale f), motive (Etale.mk f))
204+
(T : X.Etale) :
205+
motive T :=
206+
mk _ _ T.prop
207+
208+
instance : PreservesFiniteLimits (Etale.forget X) :=
209+
inferInstanceAs (PreservesFiniteLimits (MorphismProperty.Over.forget _ ⊤ X))
210+
167211
end Scheme
168212

169213
end AlgebraicGeometry

‎Mathlib/AlgebraicGeometry/Sites/Etale.lean‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,37 @@ def smallEtaleTopology (X : Scheme.{u}) : GrothendieckTopology X.Etale :=
5454
def smallEtalePretopology (X : Scheme.{u}) : Pretopology X.Etale :=
5555
X.smallPretopology (Q := @Etale) (P := @Etale)
5656

57+
set_option backward.defeqAttrib.useBackward true in
58+
set_option backward.isDefEq.respectTransparency false in
59+
lemma ofArrows_mem_smallEtaleTopology_iff
60+
{X : Scheme.{u}} {W : X.Etale} {ι : Type*}
61+
{Z : ι → X.Etale} (f : ∀ i, Z i ⟶ W) :
62+
Sieve.ofArrows _ f ∈ smallEtaleTopology _ _ ↔
63+
⋃ i, Set.range (f i).left = .univ := by
64+
refine ⟨fun hf ↦ ?_, fun hf ↦ (mem_smallGrothendieckTopology _ _).2 ?_⟩
65+
· obtain ⟨U, _, _, hU⟩ := (mem_smallGrothendieckTopology _ _).1 hf
66+
ext y
67+
simp only [Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]
68+
obtain ⟨i, ⟨u, rfl⟩⟩ := ((ofArrows_mem_precoverage_iff _).1 U.mem₀).1 y
69+
obtain ⟨_, b, _, ⟨j⟩, fac⟩ := hU _ _ ⟨i⟩
70+
replace fac : b.left ≫ (f j).left = U.f i :=
71+
(Etale.forget _ ⋙ CategoryTheory.Over.forget _).congr_map fac
72+
exact ⟨j, b.left u, by simp [← fac]⟩
73+
· have (w : W.left) : ∃ (i : ι), w ∈ Set.range (f i).left := by
74+
have := Set.mem_univ w
75+
simpa [← hf]
76+
choose i z hz using this
77+
let V : Cover (precoverage @Etale) W.left :=
78+
Cover.mkOfCovers W.left (fun w ↦ (Z (i w)).left)
79+
(fun w ↦ (f (i w)).left) (fun w ↦ ⟨_, _, hz w⟩) inferInstance
80+
letI : Cover.Over X V :=
81+
{ over w := ⟨(Z (i w)).hom⟩
82+
isOver_map w := by cat_disch }
83+
have (w : W.left) : Etale (V.X w ↘ X) := (Z (i w)).prop
84+
refine ⟨V, inferInstance, inferInstance, ?_⟩
85+
rintro _ _ ⟨w⟩
86+
refine ⟨_, 𝟙 _, _, ⟨i w⟩, by cat_disch⟩
87+
5788
instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage @Etale)) (i : 𝒰.I₀) : Etale (𝒰.f i) :=
5889
𝒰.map_prop i
5990

‎Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
/-
2+
Copyright (c) 2026 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christian Merten, Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.AlgebraicGeometry.Fiber
9+
public import Mathlib.AlgebraicGeometry.Sites.AffineEtale
10+
public import Mathlib.CategoryTheory.Functor.TypeValuedFlat
11+
public import Mathlib.CategoryTheory.Limits.Elements
12+
public import Mathlib.CategoryTheory.Sites.Point.Conservative
13+
14+
public import Mathlib.FieldTheory.SeparableClosure
15+
16+
/-!
17+
18+
# Points of the étale site
19+
20+
In this file, we show that a morphism `Spec (.of Ω) ⟶ S` where `Ω` is
21+
a separably closed field defines a point on the small étale site of `S`.
22+
We show that these points form a conservative family.
23+
24+
-/
25+
26+
@[expose] public section
27+
28+
universe u
29+
30+
open CategoryTheory Opposite
31+
32+
namespace AlgebraicGeometry.Scheme
33+
34+
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
35+
(s : Spec (.of Ω) ⟶ S)
36+
37+
lemma exists_fac_of_etale_of_isSepClosed {X S : Scheme.{u}} (f : X ⟶ S) [Etale f]
38+
{Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ S)
39+
(x : X) (hx : f x = s default) :
40+
∃ (l : Spec (.of Ω) ⟶ X), l ≫ f = s ∧ l default = x := by
41+
obtain ⟨⟨s, a⟩, rfl⟩ := (SpecToEquivOfField Ω S).symm.surjective s
42+
obtain rfl : f x = s := by simp [hx, SpecToEquivOfField]
43+
let m := (f.residueFieldMap x).hom
44+
dsimp at m
45+
algebraize [m, a.hom]
46+
let b : X.residueField x →ₐ[S.residueField (f x)] Ω :=
47+
IsSepClosed.lift
48+
have : f.residueFieldMap x ≫ CommRingCat.ofHom b.toRingHom = a := by
49+
ext1; exact b.comp_algebraMap
50+
refine ⟨Spec.map (CommRingCat.ofHom b.toRingHom) ≫ X.fromSpecResidueField x, ?_, ?_⟩
51+
· simp [SpecToEquivOfField, ← this]
52+
rfl
53+
· dsimp
54+
apply fromSpecResidueField_apply
55+
56+
instance : IsCofiltered (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).Elements :=
57+
Functor.isCofiltered_elements _
58+
59+
set_option backward.defeqAttrib.useBackward true in
60+
/-- A morphism `s : Spec (.of Ω) ⟶ S` where `Ω` is a separably closed field
61+
defines a point for the small étale site of `S`. -/
62+
@[simps]
63+
noncomputable def pointSmallEtale : (smallEtaleTopology S).Point where
64+
fiber := Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))
65+
initiallySmall :=
66+
initiallySmall_of_essentiallySmall_weakly_initial_objectProperty
67+
(Functor.Elements.precomp (AffineEtale.Spec S)
68+
(Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage (by
69+
rintro ⟨X, x⟩
70+
cases X with | _ Y f
71+
obtain ⟨y, hy, rfl⟩ := Over.homMk_surjective x
72+
dsimp at y hy
73+
obtain ⟨R, j, _, y', rfl⟩ : ∃ (R : CommRingCat) (j : Spec (.of R) ⟶ Y)
74+
(_ : IsOpenImmersion j) (y' : _ ⟶ _), y' ≫ j = y := by
75+
obtain ⟨R, j, _, hj, _⟩ := exists_affine_mem_range_and_range_subset
76+
(x := y.base default) (U := ⊤) (by simp)
77+
refine ⟨R, j, inferInstance, _, IsOpenImmersion.lift_fac j y ?_⟩
78+
rintro _ ⟨a, rfl⟩
79+
rwa [Subsingleton.elim a default]
80+
exact ⟨_,
81+
⟨Functor.elementsMk _ (AffineEtale.mk (j ≫ f)) (Over.homMk y'), ⟨Iso.refl _⟩⟩,
82+
⟨⟨MorphismProperty.Over.homMk j rfl (by simp), by cat_disch⟩⟩⟩)
83+
jointly_surjective {X} R hR φ := by
84+
cases X with | _ X f
85+
obtain ⟨φ : Spec (.of Ω) ⟶ X, rfl : φ ≫ f = s, rfl⟩ := Over.homMk_surjective φ
86+
obtain ⟨𝒰, h, _, le⟩ := (mem_smallGrothendieckTopology _ _).1 hR
87+
obtain ⟨i, y, hy⟩ := 𝒰.exists_eq (φ default)
88+
obtain ⟨l, hl₁, hl₂⟩ := exists_fac_of_etale_of_isSepClosed (𝒰.f i) φ _ hy
89+
have : 𝒰.f i ≫ f = 𝒰.X i ↘ S := HomIsOver.comp_over (f := 𝒰.f i) (S := S)
90+
exact ⟨(𝒰.X i).asOverProp S inferInstance,
91+
MorphismProperty.Over.homMk (𝒰.f i), le _ _ ⟨i⟩, Over.homMk l, by cat_disch⟩
92+
93+
variable {s₀ : S} (hs₀ : s default = s₀)
94+
95+
/-- Given a morphism `s : Spec (.of Ω) ⟶ S` with image `s₀ : S` where `Ω` is a
96+
separably closed field, this is the canonical map
97+
`(pointSmallEtale s).fiber.obj X ⟶ X.hom ⁻¹' {s₀}` for `X : S.Etale`. -/
98+
@[simps]
99+
noncomputable def pointSmallEtaleFiberObjToPreimage {X : S.Etale}
100+
(t : (pointSmallEtale s).fiber.obj X) :
101+
X.hom ⁻¹' {s₀} :=
102+
⟨t.left (default : Spec (.of Ω)), by
103+
have := (Over.w t).symm
104+
cat_disch⟩
105+
106+
set_option backward.isDefEq.respectTransparency false in
107+
instance {Y X : Scheme.{u}} (f : Y ⟶ X) [Etale f] (x : X) :
108+
Etale (f.fiberToSpecResidueField x) := by
109+
dsimp [Hom.fiberToSpecResidueField]
110+
infer_instance
111+
112+
set_option backward.isDefEq.respectTransparency false in
113+
lemma pointSmallEtaleFiberObjToPreimage_surjective (X : S.Etale) :
114+
Function.Surjective (pointSmallEtaleFiberObjToPreimage s hs₀ (X := X)) := by
115+
intro y
116+
obtain ⟨y, rfl⟩ := (X.hom.fiberHomeo s₀).surjective y
117+
obtain ⟨⟨t, a⟩, rfl⟩ := (Scheme.SpecToEquivOfField Ω _).symm.surjective s
118+
obtain rfl : t = s₀ := by simp [SpecToEquivOfField, ← hs₀]
119+
obtain ⟨l, hl, rfl⟩ := exists_fac_of_etale_of_isSepClosed
120+
(X.hom.fiberToSpecResidueField _) (Spec.map a) y (by subsingleton)
121+
refine ⟨Over.homMk (l ≫ X.hom.fiberι t) ?_, rfl⟩
122+
simp [X.hom.fiber_fac, reassoc_of% hl]
123+
rfl
124+
125+
set_option backward.isDefEq.respectTransparency false in
126+
lemma isConservative_pointSmallEtale
127+
{ι : Type*} {S : Scheme.{u}}
128+
{Ω : ι → Type u} [∀ i, Field (Ω i)] [∀ i, IsSepClosed (Ω i)]
129+
(s : ∀ i, Spec (.of (Ω i)) ⟶ S)
130+
(hs : ⋃ i, Set.range (s i) = .univ) :
131+
(ObjectProperty.ofObj (fun i ↦ pointSmallEtale (s i))).IsConservativeFamilyOfPoints :=
132+
.mk' (fun X R hR ↦ by
133+
obtain ⟨α, T, f, rfl⟩ := R.exists_eq_ofArrows
134+
rw [ofArrows_mem_smallEtaleTopology_iff]
135+
ext x
136+
simp only [Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]
137+
obtain ⟨i, hi⟩ : ∃ i, s i default = X.hom x := by
138+
have := Set.mem_univ (X.hom x)
139+
simp only [← hs, Functor.id_obj, Set.mem_iUnion, Set.mem_range] at this
140+
obtain ⟨i, y, hy⟩ := this
141+
obtain rfl := Subsingleton.elim y default
142+
exact ⟨i, hy⟩
143+
obtain ⟨x', hx'⟩ := pointSmallEtaleFiberObjToPreimage_surjective (s i) hi X ⟨x, by simp⟩
144+
rw [Subtype.ext_iff] at hx'
145+
simp only [Functor.id_obj, pointSmallEtaleFiberObjToPreimage_coe, Etale.forget_obj_left] at hx'
146+
subst hx'
147+
obtain ⟨W, g, ⟨Z, p, _, ⟨a⟩, rfl⟩, y, rfl⟩ := hR ⟨_, ⟨i⟩⟩ x'
148+
exact ⟨a, (pointSmallEtaleFiberObjToPreimage (s i) hi (y ≫ p.hom)).1, rfl⟩)
149+
150+
lemma isConservativeFamilyOfPoints_pointSmallEtale' (S : Scheme.{u}) :
151+
(ObjectProperty.ofObj (fun (s : S) ↦ pointSmallEtale
152+
((SpecToEquivOfField (SeparableClosure (S.residueField s)) _).2
153+
⟨s, CommRingCat.ofHom
154+
(algebraMap (S.residueField s) _)⟩))).IsConservativeFamilyOfPoints :=
155+
isConservative_pointSmallEtale _ (by
156+
ext s
157+
simp only [Equiv.invFun_as_coe, Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]
158+
exact ⟨s, default, by simp [SpecToEquivOfField]⟩)
159+
160+
instance : GrothendieckTopology.HasEnoughPoints.{u} (smallEtaleTopology S) where
161+
exists_objectProperty :=
162+
⟨_, inferInstance, isConservativeFamilyOfPoints_pointSmallEtale' S⟩
163+
164+
end AlgebraicGeometry.Scheme

‎Mathlib/CategoryTheory/Elements.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
public import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
99
public import Mathlib.CategoryTheory.EssentiallySmall
10+
public import Mathlib.CategoryTheory.ObjectProperty.Small
1011

1112
/-!
1213
# The category of elements
@@ -354,6 +355,26 @@ def Elements.initial (A : C) : (yoneda.obj A).Elements :=
354355
def Elements.isInitial (A : C) : Limits.IsInitial (Elements.initial A) :=
355356
isInitialOfRepresentableBy (.yoneda A)
356357

358+
/-- The functor `(F ⋙ G).Elements ⥤ G.Elements`. -/
359+
@[simps]
360+
def Elements.precomp {D : Type*} [Category D] (F : C ⥤ D) (G : D ⥤ Type w) :
361+
(F ⋙ G).Elements ⥤ G.Elements where
362+
obj x := G.elementsMk (F.obj x.fst) x.snd
363+
map f := ⟨F.map f.1, f.2⟩
364+
365+
instance Elements.essentiallySmall {C : Type u} [Category.{v} C]
366+
(F : C ⥤ Type w) [EssentiallySmall.{w} C] :
367+
EssentiallySmall.{w} F.Elements := by
368+
rw [essentiallySmall_iff_objectPropertyEssentiallySmall_top]
369+
obtain ⟨P, _, hP⟩ := ObjectProperty.EssentiallySmall.exists_small_le' (⊤ : ObjectProperty C)
370+
refine ⟨fun x ↦ P x.1, ?_, fun y _ ↦ ?_⟩
371+
· exact small_of_surjective.{w} (α := Σ (Z : Subtype P), F.obj Z.1)
372+
(f := fun x ↦ ⟨F.elementsMk _ x.2, x.1.2⟩)
373+
(fun ⟨x, hx⟩ ↦ ⟨⟨⟨x.1, hx⟩, x.2⟩, rfl⟩)
374+
· obtain ⟨Z, hZ, ⟨e⟩⟩ := hP y.fst (by simp)
375+
exact ⟨F.elementsMk Z (F.map e.hom y.snd), hZ,
376+
⟨CategoryOfElements.isoMk _ _ e rfl⟩⟩
377+
357378
end Functor
358379

359380
end CategoryTheory

‎Mathlib/CategoryTheory/EssentialImage.lean‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,9 @@ Authors: Bhavik Mehta
55
-/
66
module
77

8-
public import Mathlib.CategoryTheory.NatIso
98
public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
109
public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
11-
public import Mathlib.Data.Set.Operations
10+
public import Mathlib.Order.BooleanAlgebra.Defs
1211

1312
/-!
1413
# Essential image of a functor
@@ -223,4 +222,13 @@ lemma faithful_of_comp_essSurj (F : D ⥤ E) (L : C ⥤ D) [EssSurj L]
223222

224223
end Functor
225224

225+
lemma ObjectProperty.map_top (F : C ⥤ D) :
226+
(⊤ : ObjectProperty C).map F = F.essImage := by
227+
ext Y
228+
refine ⟨?_, ?_⟩
229+
· rintro ⟨X, _, ⟨e⟩⟩
230+
exact ⟨X, ⟨e⟩⟩
231+
· rintro ⟨X, ⟨e⟩⟩
232+
exact ⟨X, by simp, ⟨e⟩⟩
233+
226234
end CategoryTheory

‎Mathlib/CategoryTheory/Limits/FinallySmall.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,17 @@ theorem initiallySmall_of_small_weakly_initial_set [IsCofilteredOrEmpty J] (s :
212212
obtain ⟨j, hj₁, hj₂⟩ := hs i
213213
exact ⟨⟨j, hj₁⟩, hj₂⟩
214214

215+
variable {J} in
216+
theorem initiallySmall_of_essentiallySmall_weakly_initial_objectProperty
217+
[IsCofilteredOrEmpty J] (P : ObjectProperty J) [ObjectProperty.EssentiallySmall.{v} P]
218+
(hP : ∀ i, ∃ j, P j ∧ Nonempty (j ⟶ i)) : InitiallySmall.{v} J := by
219+
obtain ⟨Q, H, hQ⟩ := ObjectProperty.EssentiallySmall.exists_small_le'.{v} P
220+
have : Small.{v} (show Set _ from Q) := by assumption
221+
refine initiallySmall_of_small_weakly_initial_set Q (fun i ↦ ?_)
222+
obtain ⟨j, hj, ⟨f⟩⟩ := hP i
223+
obtain ⟨k, hk, ⟨e⟩⟩ := hQ _ hj
224+
exact ⟨k, hk, ⟨e.inv ≫ f⟩⟩
225+
215226
theorem initiallySmall_iff_exists_small_weakly_initial_set [IsCofilteredOrEmpty J] :
216227
InitiallySmall.{v} J ↔ ∃ (s : Set J) (_ : Small.{v} s), ∀ i, ∃ j ∈ s, Nonempty (j ⟶ i) := by
217228
refine ⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩

‎Mathlib/CategoryTheory/Limits/MorphismProperty.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,9 +296,12 @@ instance (priority := 900) hasPullbacks [HasPullbacks T] [P.IsStableUnderComposi
296296
[P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] : HasPullbacks (P.Over ⊤ X) :=
297297
CostructuredArrow.hasPullbacks _ _
298298

299-
variable [HasPullbacks T] [P.IsStableUnderComposition] [P.ContainsIdentities]
299+
variable [HasPullbacks T] [P.IsMultiplicative]
300300
[P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P]
301301

302+
instance hasFiniteLimits : HasFiniteLimits (P.Over ⊤ X) :=
303+
hasFiniteLimits_of_hasTerminal_and_pullbacks
304+
302305
noncomputable instance : CreatesFiniteLimits (Over.forget P ⊤ X) :=
303306
createsFiniteLimitsOfCreatesTerminalAndPullbacks _
304307

‎Mathlib/CategoryTheory/MorphismProperty/Comma.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -790,7 +790,7 @@ lemma CostructuredArrow.Hom.ext {A B : P.CostructuredArrow Q F X} {f g : A ⟶ B
790790
ext <;> simp [h]
791791

792792
variable {P Q F X} in
793-
/-- Construct an morphism in `P.CostructuredArrow Q F X` by giving the isomorphism
793+
/-- Construct an isomorphism in `P.CostructuredArrow Q F X` by giving the isomorphism
794794
on the underlying objects of `C`. -/
795795
@[simps]
796796
def CostructuredArrow.isoMk {A B : P.CostructuredArrow Q F X} (f : A.left ≅ B.left) (hf : Q f.hom)

0 commit comments

Comments
 (0)