instRepresentablyFlatOpensCarrierMap

English

The map on opens induced by f is representably flat.

Русский

Образ открытых множеств, индуцируемый отображением f, является representably flat.

LaTeX

$$$\operatorname{RepresentablyFlat}(\operatorname{Opens.map} f)$$$

Lean4

instance : RepresentablyFlat (Opens.map f) := by
  constructor
  intro U
  refine @IsCofiltered.mk _ _ ?_ ?_
  · constructor
    · intro V W
      exact
        ⟨⟨⟨PUnit.unit⟩, V.right ⊓ W.right, homOfLE <| le_inf V.hom.le W.hom.le⟩,
          StructuredArrow.homMk (homOfLE inf_le_left), StructuredArrow.homMk (homOfLE inf_le_right), trivial⟩
    · exact fun _ _ _ _ ↦ ⟨_, 𝟙 _, by simp [eq_iff_true_of_subsingleton]⟩
  · exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

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