English
Under suitable hypotheses, IsLocallyInjective J (whiskerLeft H.op f) is equivalent to IsLocallyInjective K f.
Русский
При подходящих предположениях локальная инъективность для whiskerLeft эквивалентна локальной инъективности для f над K.
LaTeX
$$$IsLocallyInjective J (H.op.whiskerLeft f) \iff IsLocallyInjective K f$$$
Lean4
theorem isLocallyInjective_of_whisker (hH : CoverPreserving J K H) [H.IsCoverDense K]
[IsLocallyInjective J (whiskerLeft H.op f)] : IsLocallyInjective K f where
equalizerSieve_mem {X} a b
h := by
apply K.transitive (H.is_cover_of_isCoverDense K X.unop)
intro Y g ⟨⟨Z, lift, m, fac⟩⟩
rw [← fac, Sieve.pullback_comp]
apply K.pullback_stable
refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_
refine
K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
(hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f) (F.map m.op a) (F.map m.op b) ?_)
· intro W q hq
simpa using hq
· simp only [comp_obj, op_obj, whiskerLeft_app, Opposite.op_unop]
rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]
