LeanPool.WhiteheadTheorem.Shapes.Pushout #

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.Pushout.

TODO:

Dualize some of the results in Mathlib.Topology.Category.TopCat.Limits.Pullbacks to give explicit descriptions of the topology on pushouts.
Simplify the proofs in this file using Mathlib.CategoryTheory.Limits.Types.

theorem TopCat.pushout_isOpen {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (s : Set ↑(CategoryTheory.Limits.pushout f g)) (hl : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inl f g)) ⁻¹' s)) (hr : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g)) ⁻¹' s)) :

IsOpen s

Explicit description of the topology on the pushout

source

@[reducible, inline]

abbrev TopCat.homToDiscreteSpaceOfFun {X : TopCat} {Y : Type u} (f : ↑X → Y) :

X ⟶ of Y

Construct a morphism into a discrete space Y using a function into Y.

Equations

TopCat.homToDiscreteSpaceOfFun f = TopCat.ofHom { toFun := f, continuous_toFun := ⋯ }

Instances For

source

theorem TopCat.eq_inl_or_eq_inr_of_mem_pushout {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (a : ↑(CategoryTheory.Limits.pushout f g)) :

(∃ (y : ↑Y), a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inl f g)) y) ∨ ∃ (z : ↑Z), a = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g)) z

In the pushout square below, the image of inl and the image of inr cover the space (pushout f g).carrier.

X ----f----> Y
|            |
g           inl
|            |
v            v
Z ---inr---> pushout f g

source

@[reducible, inline]

noncomputable abbrev TopCat.pushoutInr' {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) :

C(↑(Set.range ⇑(CategoryTheory.ConcreteCategory.hom g))ᶜ, ↑(CategoryTheory.Limits.pushout f g))

pushoutInr'

Equations

TopCat.pushoutInr' f g = ContinuousMap.restrict (Set.range ⇑(CategoryTheory.ConcreteCategory.hom g))ᶜ (TopCat.Hom.hom (CategoryTheory.Limits.pushout.inr f g))

Instances For

source

theorem TopCat.injective_pushoutInr' {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) :

Function.Injective ⇑(pushoutInr' f g)

In the pushout square below, the map inr restricted to {z | z ∉ Set.range g} is injective.

X ----f----> Y
|            |
g           inl
|            |
v            v
Z ---inr---> pushout f g

The proof is similar to the one in https://math.stackexchange.com/questions/3906319/pushout-of-injective-is-injective TODO: prove this in the category of types.

source

theorem TopCat.pushoutInr_neq_pushoutInr_of_mem_compl_range_of_mem_range {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (z : ↑Z) :

z ∈ (Set.range ⇑(CategoryTheory.ConcreteCategory.hom g))ᶜ → ∀ z' ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g)) z ≠ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g)) z'

source

theorem TopCat.pushoutInr_neq_pushoutInl_of_mem_compl_range {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (z : ↑Z) :

z ∈ (Set.range ⇑(CategoryTheory.ConcreteCategory.hom g))ᶜ → ∀ (y : ↑Y), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inr f g)) z ≠ (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pushout.inl f g)) y

TODO: re-use the code in pushoutInr_neq_pushoutInr_of_mem_compl_range_of_mem_range

source

theorem Function.Injective.preimage_image_of_restrict (X Y : Type u) (A : Set X) (s : Set ↑A) (f : X → Y) (inj_f : Injective (A.restrict f)) (hf : ∀ a ∈ A, ∀ b ∉ A, f a ≠ f b) :

f ⁻¹' A.restrict f '' s = Subtype.val '' s

source

theorem TopCat.isOpenMap_pushoutInr' {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (hg : IsClosed {z : ↑Z | z ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)}) :

IsOpenMap ⇑(pushoutInr' f g)

In the pushout square below, if g X is closed in Z, then the map inr restricted to {z | z ∉ Set.range g} is an open map.

X ----f----> Y
|            |
g           inl
|            |
v            v
Z ---inr---> pushout f g

source

theorem TopCat.isOpenEmbedding_pushoutInr' {X Y Z : TopCat} (f : X ⟶ Y) (g : X ⟶ Z) (hg : IsClosed {z : ↑Z | z ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)}) :

Topology.IsOpenEmbedding ⇑(pushoutInr' f g)

In the pushout square below, if g X is closed in Z, then the map inr restricted to {z | z ∉ Set.range g} is an open embedding.

X ----f----> Y
|            |
g           inl
|            |
v            v
Z ---inr---> pushout f g