liftCoborder_preimage — Mathlib

English

For an immersion f and an open U in coborderRange f, the evaluated liftCoborder on U equals the composition of f.app on the image of U with the presheaf map along the appropriate eqToHom.

Русский

Для вложения f и открытого множества U в coborderRange f значение liftCoborder на U равно композиции f.app на образе U с отображением из прешейф по соответствующему eqToHom.

LaTeX

$$$f.liftCoborder.app\\,U = f.app\\, (f.coborderRange.ι ''ᵁ U) \\circ X.presheaf.map (eqToHom (\\text{...}).op)$$$

Lean4

theorem liftCoborder_preimage [IsImmersion f] (U : f.coborderRange.toScheme.Opens) :
    f.liftCoborder ⁻¹ᵁ U = f ⁻¹ᵁ f.coborderRange.ι ''ᵁ U :=
  by
  conv_rhs => enter [1]; rw [← f.liftCoborder_ι]
  rw [Scheme.preimage_comp, Scheme.Hom.preimage_image_eq]

Похожие утверждения