From c120b6b380ceadd127cab2fdec4d8ad5bb635861 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Wed, 6 May 2026 09:17:30 -0600 Subject: [PATCH 1/2] chore(Topology/Category): make TopCat.Hom constructor private --- Mathlib/Condensed/Light/Sequence.lean | 14 ++++++++------ Mathlib/Topology/Category/TopCat/Basic.lean | 6 +++++- Mathlib/Topology/Category/TopPair.lean | 2 +- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/Mathlib/Condensed/Light/Sequence.lean b/Mathlib/Condensed/Light/Sequence.lean index 541eb9ab95c7af..3d3925d90f5d93 100644 --- a/Mathlib/Condensed/Light/Sequence.lean +++ b/Mathlib/Condensed/Light/Sequence.lean @@ -32,7 +32,7 @@ def LightProfinite.fibre : LightProfinite := isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact of (f ⁻¹' {y}) -def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨⟨{ toFun := Subtype.val }⟩⟩ +def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨TopCat.ofHom { toFun := Subtype.val }⟩ end @@ -190,9 +190,9 @@ are equal. This can be checked by precomposing with an epimorphism, which is given by this morphism. -/ def cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : (of _ (T ⊕ (pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) - (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨⟨{ + (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨TopCat.ofHom { toFun := coverToFun _ _ - continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩⟩ + continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩ open Limits in set_option backward.isDefEq.respectTransparency false in @@ -262,7 +262,9 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : -- `fibres`. have := S'_compactSpace π (by fun_prop) let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ LightProfinite.fibre n (π ≫ snd _ _) := - ⟨⟨{ toFun x := x.val n, continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩⟩ + ⟨TopCat.ofHom { + toFun x := x.val n, + continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩ let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩ let π' := pullback.snd π (y' ▷ ℕ∪{∞}) let σ' : ℕ∪{∞} → LightProfinite.of (S' π) → pullback π (y' ▷ ℕ∪{∞}) := fun n ↦ @@ -276,8 +278,8 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : have : CompactSpace (fibres π' σ') := isCompact_iff_compactSpace.mp (fibres_closed π' (by fun_prop) σ' (by fun_prop) hσ').isCompact refine ⟨LightProfinite.of (S' π), LightProfinite.of (fibres π' σ'), y', - ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ π', - ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩ + ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ π', + ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩ · rw [LightProfinite.epi_iff_surjective] refine fibres_surjective _ ?_ _ hσ hσ' rw [← LightProfinite.epi_iff_surjective] diff --git a/Mathlib/Topology/Category/TopCat/Basic.lean b/Mathlib/Topology/Category/TopCat/Basic.lean index 314d465ed09a31..6b539b26b73783 100644 --- a/Mathlib/Topology/Category/TopCat/Basic.lean +++ b/Mathlib/Topology/Category/TopCat/Basic.lean @@ -67,15 +67,19 @@ variable {X} in /-- The type of morphisms in `TopCat`. -/ @[ext] structure Hom (X Y : TopCat.{u}) where - --private mk :: + private mk :: /-- The underlying `ContinuousMap`. -/ hom' : C(X, Y) +set_option backward.privateInPublic true in +set_option backward.privateInPublic.warn false in instance : Category TopCat where Hom X Y := Hom X Y id X := ⟨ContinuousMap.id X⟩ comp f g := ⟨g.hom'.comp f.hom'⟩ +set_option backward.privateInPublic true in +set_option backward.privateInPublic.warn false in instance : ConcreteCategory.{u} TopCat (fun X Y => C(X, Y)) where hom := Hom.hom' ofHom f := ⟨f⟩ diff --git a/Mathlib/Topology/Category/TopPair.lean b/Mathlib/Topology/Category/TopPair.lean index 0ab7c2198d79c0..b2637bd14f5d58 100644 --- a/Mathlib/Topology/Category/TopPair.lean +++ b/Mathlib/Topology/Category/TopPair.lean @@ -52,7 +52,7 @@ abbrev of {A X : TopCat.{u}} (f : A ⟶ X) (h : Topology.IsEmbedding f) : TopPai /-- Constructor for a topological pair (X, A) where A ⊆ X. -/ abbrev ofSubset {X : TopCat.{u}} (A : Set X) : TopPair.{u} := TopPair.of (A := (TopCat.of A)) - (X := X) ⟨{ toFun := Subtype.val }⟩ Topology.IsEmbedding.subtypeVal + (X := X) (TopCat.ofHom { toFun := Subtype.val }) Topology.IsEmbedding.subtypeVal /-- Constructs the topological pair `(X, ∅)` from `X : TopCat`. -/ abbrev ofTopCat (X : TopCat.{u}) : TopPair.{u} := From feae6172b2da35db695f59c145da920e1cdadb9e Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Wed, 6 May 2026 09:23:40 -0600 Subject: [PATCH 2/2] fix error --- Mathlib/Topology/Sheaves/LocalPredicate.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Sheaves/LocalPredicate.lean b/Mathlib/Topology/Sheaves/LocalPredicate.lean index ce9ba2712e09b1..3b5f28bb6a914b 100644 --- a/Mathlib/Topology/Sheaves/LocalPredicate.lean +++ b/Mathlib/Topology/Sheaves/LocalPredicate.lean @@ -361,8 +361,8 @@ the presheaf of continuous functions. def subpresheafContinuousPrelocalIsoPresheafToTop {X : TopCat.{u}} (T : TopCat.{u}) : subpresheafToTypes (continuousPrelocal X T) ≅ presheafToTop X T := NatIso.ofComponents fun X ↦ - { hom := ↾(by rintro ⟨f, c⟩; exact ofHom ⟨f, c⟩) - inv := ↾(by rintro ⟨f, c⟩; exact ⟨f, c⟩) } + { hom := ↾fun f ↦ ofHom ⟨f.1, f.2⟩ + inv := ↾fun f ↦ ⟨f.1, f.1.2⟩ } /-- The sheaf of continuous functions on `X` with values in a space `T`. -/