English
There is a nonempty SMulCandidate for each data α, φ, r, m, built from a finite intersection of image sieves and a separated presheaf condition.
Русский
Для любых данных существует непустой SMulCandidate, сконструированный через пересечение образов сеток изображений и условие разделимости прешейфа.
LaTeX
$$$ Nonempty (SMulCandidate α φ r m) $$$
Lean4
/-- Constructor for `SMulCandidate`. -/
def mk' (S : Sieve X.unop) (hS : S ∈ J X.unop) (r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget _) S.arrows)
(m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget _) S.arrows)
(hr₀ : (r₀.map (whiskerRight α (forget _))).IsAmalgamation r)
(hm₀ : (m₀.map (whiskerRight φ (forget _))).IsAmalgamation m) (a : A.val.obj X)
(ha : ((r₀.smul m₀).map (whiskerRight φ (forget _))).IsAmalgamation a) : SMulCandidate α φ r m
where
x := a
h Y f a₀ ha₀ b₀
hb₀ := by
apply A.isSeparated _ _ (J.pullback_stable f.unop hS)
rintro Z g hg
dsimp at hg
rw [← ConcreteCategory.comp_apply, ← A.val.map_comp, ← NatTrans.naturality_apply (D := Ab)]
erw [M₀.map_smul] -- Mismatch between `M₀.map` and `M₀.presheaf.map`
refine (ha _ hg).trans (app_eq_of_isLocallyInjective α φ A.isSeparated _ _ _ _ ?_ ?_)
· rw [← RingCat.comp_apply, NatTrans.naturality, RingCat.comp_apply, ha₀]
apply (hr₀ _ hg).symm.trans
simp
· erw [NatTrans.naturality_apply φ, hb₀]
apply (hm₀ _ hg).symm.trans
dsimp
rw [Functor.map_comp]
rfl
