sieve₁_eq_pullback_sieve₁' — Mathlib

English

sieve1' equals the pullback-form sieve1 for i1,i2 with HasPullback.

Русский

sieve1' совпадает с формой pullback sieve1 для i1,i2 при HasPullback.

LaTeX

$$$ E.sieve_1' i_1 i_2 = E.sieve_1( pullback.fst (E.f i_1) (E.f i_2), pullback.snd (E.f i_1) (E.f i_2) )$$$

Lean4

theorem sieve₁_eq_pullback_sieve₁' {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂) :
    E.sieve₁ p₁ p₂ = (E.sieve₁' i₁ i₂).pullback (pullback.lift _ _ w) :=
  by
  ext Z g
  constructor
  · rintro ⟨j, h, fac₁, fac₂⟩
    exact ⟨_, h, _, ⟨j⟩, by cat_disch⟩
  · rintro ⟨_, h, w, ⟨j⟩, fac⟩
    exact ⟨j, h, by simpa using fac.symm =≫ pullback.fst _ _, by simpa using fac.symm =≫ pullback.snd _ _⟩

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