English
Given a LocalInvariantProp P between groupoids G,G' and charted spaces M,M', there is a derived local predicate on maps from M to M' defined by LiftProp P.
Русский
Для локального инвариантного свойства P между группоидиями G,G' и чарти-спейсами M,M' существует локальное предикатное преобразование на отображениях M→M', задаваемое LiftProp P.
LaTeX
$$localPredicate hG : TopCat.LocalPredicate (fun _ => M')$$
Lean4
/-- Let `P` be a `LocalInvariantProp` for functions between spaces with the groupoids `G`, `G'`
and let `M`, `M'` be charted spaces modelled on the model spaces of those groupoids. Then there is
an induced `LocalPredicate` on the functions from `M` to `M'`, given by `LiftProp P`. -/
def localPredicate (hG : LocalInvariantProp G G' P) : TopCat.LocalPredicate fun _ : TopCat.of M => M'
where
pred {U : Opens (TopCat.of M)} := fun f : U → M' => ChartedSpace.LiftProp P f
res := by
intro U V i f h x
have hUV : U ≤ V := CategoryTheory.leOfHom i
change ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
rw [← hG.liftPropAt_iff_comp_inclusion hUV]
apply h
locality := by
intro V f h x
obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ _)⟩ := h x
let x' : U := ⟨x, hxU⟩
have hUV : U ≤ V := CategoryTheory.leOfHom i
have : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x') :=
by
rw [hG.liftPropAt_iff_comp_inclusion hUV]
exact hU x'
convert this
