isLocallySurjective_iff_epi' — Mathlib

English

The pre-coverage associated to a Grothendieck topology is stable under base change.

Русский

Связанное предпокрытие топологии Гротендикa устойчиво к базовым изменениям.

LaTeX

$$$$ J.toPrecoverage.IsStableUnderBaseChange $$$$

Lean4

theorem isLocallySurjective_iff_epi' : IsLocallySurjective φ ↔ Epi φ :=
  by
  constructor
  · intro
    infer_instance
  · intro
    let data := (locallySurjective J A).factorizationData (locallyInjective J A) φ
    have : IsLocallySurjective data.i := data.hi
    have : IsLocallyInjective data.p := data.hp
    have : Epi data.p := epi_of_epi_fac data.fac
    have := mono_of_isLocallyInjective data.p
    have := isIso_of_mono_of_epi data.p
    rw [← data.fac]
    infer_instance

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