Commit 2023-10-20 14:35 93521b73

View on Github →

feat: condensed sets are equivalent to sheaves on Stonean and Profinite (#6810)

depends on: #6809

Estimated changes

Modified Mathlib.lean

Created Mathlib/Condensed/Equivalence.lean

added def Condensed.ProfiniteCompHaus.equivalence

added theorem Condensed.StoneanCompHaus.coherentTopology_is_induced

added theorem Condensed.StoneanCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily

added theorem Condensed.StoneanCompHaus.coverDense

added theorem Condensed.StoneanCompHaus.coverLifting

added theorem Condensed.StoneanCompHaus.coverPreserving

added def Condensed.StoneanCompHaus.equivalence

added theorem Condensed.StoneanCompHaus.generate_singleton_mem_coherentTopology

added theorem Condensed.StoneanProfinite.coherentTopology_is_induced

added theorem Condensed.StoneanProfinite.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily

added theorem Condensed.StoneanProfinite.coverDense

added theorem Condensed.StoneanProfinite.coverLifting

added theorem Condensed.StoneanProfinite.coverPreserving

added def Condensed.StoneanProfinite.equivalence

added theorem Condensed.StoneanProfinite.generate_singleton_mem_coherentTopology