Commit 2026-06-05 16:26 855dbcc1

refactor(CategoryTheory/Sites): replace Functor.inducedTopology (#39951) The current Functor.inducedTopology is only defined for a locally fully faithful and locally cover dense functor and in the general situation it does not make the functor continuous. We change the situation in two ways:

• Replace Functor.inducedTopology by the induced topology in the sense of SGA, III, 3.1: The finest topology on the domain making a functor continuous.
• Add Functor.restrictedTopology: This is the coarsest topology on the domain containing all sieves whose image generates a covering sieve in the codomain. In general, a functor does not preserve covers for this topology and in particular is not necessarily continuous. The old Functor.inducedTopology is equal (but not def-eq) to the new Functor.restrictedTopology whenever the old definition applies. In the situation where Functor.restrictedTopology makes the functor continuous, for example when F is flat, locally fully faithful and locally cover dense, the two topologies agree. Related Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Induced.20topology.20on.20a.20category/with/593098526 From Proetale.