W_eq_inverseImage_isomorphisms_of_adjunction

English

Equality of W with the inverse image of isomorphisms under an adjunction G: W = isomorphisms.inverseImage G.

Русский

Равенство W и обратная образность изоморфизмов по отображению G при сопряжении.

LaTeX

$$$J.W = (\operatorname{MorphismProperty.isomorphisms}_\{\_\}).inverseImage G.$$$

Lean4

theorem W_eq_inverseImage_isomorphisms_of_adjunction (adj : G ⊣ sheafToPresheaf J A) :
    J.W = (MorphismProperty.isomorphisms _).inverseImage G := by
  rw [W_eq_W_range_sheafToPresheaf_obj, LeftBousfield.W_eq_inverseImage_isomorphisms adj]

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