instIsDenseSubsiteInducedTopologyInverseFunctor

English

An equivalence induces a dense subsite on the target from the source Grothendieck topology via the inverse functor, and this subsite preserves covers.

Русский

Эквивалентность индуцирует плотную подсайт на целевой категории через обратную функторность, и этот подсайт сохраняет покрытия.

LaTeX

$$$e.functor.IsDenseSubsite J (e.inverse.inducedTopology J)$$$

Lean4

instance : e.functor.IsDenseSubsite J (e.inverse.inducedTopology J) :=
  by
  have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) :=
    by
    ext X S
    rw [show S ∈ (e.functor.inducedTopology (e.inverse.inducedTopology J)) X ↔ _ from
        (GrothendieckTopology.pullback_mem_iff_of_isIso (i := e.unit.app X)).symm]
    congr!; ext Y f; simp
  nth_rw 1 [this]
  infer_instance

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