instIsCoverDenseOfIsEquivalence — Mathlib

English

Equivalence provides equality of induced topologies under certain dense subsite conditions.

Русский

Эквивалентность обеспечивает равенство индуцированных топологий при подходящих условиях плотности подграждан.

LaTeX

$$$K = e.inverse.inducedTopology J$ under dense subsite$$

Lean4

instance (priority := 900) [G.IsEquivalence] : IsCoverDense G J where
  is_cover
    U := by
    let e := (asEquivalence G).symm
    convert J.top_mem U
    ext Y f
    simp only [Sieve.top_apply, iff_true]
    let g : e.inverse.obj _ ⟶ U := (e.unitInv.app Y) ≫ f
    have : (Sieve.coverByImage e.inverse U).arrows g := Presieve.in_coverByImage _ g
    replace := Sieve.downward_closed _ this (e.unit.app Y)
    simpa [g] using this

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