W_eq_inverseImage_isomorphisms — Mathlib

English

Equality J.W = (MorphismProperty.isomorphisms _).inverseImage (presheafToSheaf J A).

Русский

Равенство J.W = inverseImage изоморфизм под presheafToSheaf J A.

LaTeX

$$$J.W = (\operatorname{MorphismProperty.isomorphisms}(\mathrm{presheafToSheaf}(J,A))).inverseImage(\mathrm{presheafToSheaf}(J,A)).$$$

Lean4

theorem W_eq_inverseImage_isomorphisms : J.W = (MorphismProperty.isomorphisms _).inverseImage (presheafToSheaf J A) :=
  J.W_eq_inverseImage_isomorphisms_of_adjunction (sheafificationAdjunction J A)

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