W_eq_W_range_sheafToPresheaf_obj — Mathlib

English

Equality of the W-coverage with the inverse image of isomorphisms under an adjoint G: J.W = IsomInverseImage G.

Русский

Равенство покрытия W и обратной образности изоморфизмов под отображением G, сопряжённым кAdjunction.

LaTeX

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

Lean4

theorem W_eq_W_range_sheafToPresheaf_obj : J.W = LeftBousfield.W (· ∈ Set.range (sheafToPresheaf J A).obj) :=
  by
  apply congr_arg
  ext P
  constructor
  · intro hP
    exact ⟨⟨P, hP⟩, rfl⟩
  · rintro ⟨F, rfl⟩
    exact F.cond

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