The wedge sum of a family of pointed spaces

The wedge sum ⋁ᵢ Xᵢ of a family of pointed spaces (Xᵢ, xᵢ) is the disjoint union of the Xᵢ with all the base points xᵢ identified to a single wedge point, carrying the quotient topology. A wedge of circles is the basic example: its fundamental group is the free group on the circles, computed from the Seifert--van Kampen theorem in TauCeti.AlgebraicTopology.FundamentalGroup.WedgeSum.

The wedge point is added as a separate point before taking the quotient, so the wedge sum of the empty family is a point rather than empty. Concretely the wedge sum is the quotient of Unit ⊕ Σ i, X i by the kernel of the normalization which replaces each base point by the extra point; the quotient presentation is private, and the wedge sum is used through the wedge point TauCeti.WedgeSum.base, the inclusions TauCeti.WedgeSum.incl of the summands, which points they identify (TauCeti.WedgeSum.incl_eq_incl_iff), the induction principle TauCeti.WedgeSum.ind and the universal property TauCeti.WedgeSum.lift.

Main declarations

• TauCeti.WedgeSum: the wedge sum of a family of pointed spaces, with its wedge point TauCeti.WedgeSum.base and the inclusions TauCeti.WedgeSum.incl of the summands.
• TauCeti.WedgeSum.isOpen_iff: a set is open exactly when its preimage in every summand is.
• TauCeti.WedgeSum.lift: the universal property, with TauCeti.WedgeSum.hom_ext, and TauCeti.WedgeSum.liftProd, its form for maps out of Z × ⋁ᵢ Xᵢ, which builds homotopies out of a wedge sum.
• TauCeti.WedgeSum.subtypeVal and TauCeti.WedgeSum.isOpenEmbedding_subtypeVal: the wedge sum of open neighbourhoods of the base points is an open subspace of the whole wedge sum.
• TauCeti.WedgeSum.proj: the retraction of a wedge sum onto one summand, collapsing the others to the base point.

References

• A. Hatcher, Algebraic Topology, Chapter 0, the wedge sum in "Operations on spaces".

def TauCeti.WedgeSum {ι : Type u} {X : ι → Type v} (x : (i : ι) → X i) : Type (max u v)

The wedge sum of the pointed spaces (X i, x i): their disjoint union with all the base points identified to one wedge point. It carries the quotient topology, and the wedge sum of the empty family is a point.

The presentation as a quotient is private: points of the wedge sum come from TauCeti.WedgeSum.base and TauCeti.WedgeSum.incl, which points they identify from TauCeti.WedgeSum.incl_eq_incl_iff and TauCeti.WedgeSum.incl_eq_base_iff, maps out of it from TauCeti.WedgeSum.lift, and statements about all of its points from TauCeti.WedgeSum.ind.

Equations

• TauCeti.WedgeSum x = Quotient (Setoid.ker (TauCeti.wedgeNormalize✝ x))

The topology is transported from the private quotient; the instance is @[no_expose], which is what lets its body name the private constant.

@[instance_reducible]

instance TauCeti.WedgeSum.instTopologicalSpace {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} : TopologicalSpace (WedgeSum x)

Equations

• TauCeti.WedgeSum.instTopologicalSpace = { IsOpen := TauCeti.WedgeSum.instTopologicalSpace._aux_1✝, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

noncomputable def TauCeti.WedgeSum.base {ι : Type u} {X : ι → Type v} (x : (i : ι) → X i) : WedgeSum x

The wedge point of the wedge sum, to which all the base points are glued.

Equations

• TauCeti.WedgeSum.base x = ⟦Sum.inl ()⟧

noncomputable def TauCeti.WedgeSum.incl {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) (i : ι) : C(X i, WedgeSum x)

The inclusion of the i-th summand into the wedge sum.

Equations

• TauCeti.WedgeSum.incl x i = { toFun := fun (y : X i) => ⟦Sum.inr ⟨i, y⟩⟧, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.WedgeSum.incl_eq_base_iff {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {i : ι} {y : X i} : (incl x i) y = base x ↔ y = x i

A point of a summand is glued to the wedge point exactly when it is the base point.

@[simp]

theorem TauCeti.WedgeSum.incl_apply_self {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} (i : ι) : (incl x i) (x i) = base x

The base point of every summand is glued to the wedge point.

theorem TauCeti.WedgeSum.incl_eq_incl_iff {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {i j : ι} {y : X i} {z : X j} : (incl x i) y = (incl x j) z ↔ y = x i ∧ z = x j ∨ ⟨i, y⟩ = ⟨j, z⟩

Points of two summands are identified in the wedge sum exactly when both are base points or they are the same point of the same summand.

@[simp]

theorem TauCeti.WedgeSum.incl_inj {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {i : ι} {y z : X i} : (incl x i) y = (incl x i) z ↔ y = z

theorem TauCeti.WedgeSum.incl_injective {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} (i : ι) : Function.Injective ⇑(incl x i)

theorem TauCeti.WedgeSum.ind {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {p : WedgeSum x → Prop} (base : p (base x)) (incl : ∀ (i : ι) (y : X i), p ((incl x i) y)) (w : WedgeSum x) : p w

Every point of the wedge sum is the wedge point or comes from a summand.

@[instance_reducible]

noncomputable instance TauCeti.WedgeSum.instInhabited {ι : Type u} {X : ι → Type v} {x : (i : ι) → X i} : Inhabited (WedgeSum x)

Equations

• TauCeti.WedgeSum.instInhabited = { default := TauCeti.WedgeSum.base x }

instance TauCeti.WedgeSum.instSubsingletonOfIsEmpty {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} [IsEmpty ι] : Subsingleton (WedgeSum x)

The wedge sum of the empty family is a point.

theorem TauCeti.WedgeSum.isQuotientMap_sumElim {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} : Topology.IsQuotientMap (Sum.elim (fun (x_1 : Unit) => base x) fun (q : (i : ι) × X i) => (incl x q.fst) q.snd)

The wedge sum is a quotient of Unit ⊕ Σ i, X i.

theorem TauCeti.WedgeSum.isOpen_iff {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : Set (WedgeSum x)} : IsOpen S ↔ ∀ (i : ι), IsOpen (⇑(incl x i) ⁻¹' S)

A subset of the wedge sum is open exactly when its preimage in every summand is open.

noncomputable def TauCeti.WedgeSum.lift {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] (f : (i : ι) → C(X i, Y)) (y : Y) (hf : ∀ (i : ι), (f i) (x i) = y) : C(WedgeSum x, Y)

The universal property of the wedge sum. Maps out of the summands which send every base point to the same point assemble into a map out of the wedge sum.

Equations

• TauCeti.WedgeSum.lift f y hf = { toFun := Quotient.lift (Sum.elim (fun (x : Unit) => y) fun (q : (i : ι) × X i) => (f q.fst) q.snd) ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.WedgeSum.lift_incl {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] (f : (i : ι) → C(X i, Y)) (y : Y) (hf : ∀ (i : ι), (f i) (x i) = y) (i : ι) (z : X i) : (lift f y hf) ((incl x i) z) = (f i) z

@[simp]

theorem TauCeti.WedgeSum.lift_base {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] (f : (i : ι) → C(X i, Y)) (y : Y) (hf : ∀ (i : ι), (f i) (x i) = y) : (lift f y hf) (base x) = y

theorem TauCeti.WedgeSum.hom_ext {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] {f g : C(WedgeSum x, Y)} (hbase : f (base x) = g (base x)) (h : ∀ (i : ι), f.comp (incl x i) = g.comp (incl x i)) : f = g

Extensionality for maps out of the wedge sum. Two maps out of the wedge sum which agree at the wedge point and on every summand are equal.

theorem TauCeti.WedgeSum.hom_ext_iff {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] {f g : C(WedgeSum x, Y)} : f = g ↔ f (base x) = g (base x) ∧ ∀ (i : ι), f.comp (incl x i) = g.comp (incl x i)

noncomputable def TauCeti.WedgeSum.liftProd {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] {Z : Type u_1} [TopologicalSpace Z] [LocallyCompactSpace Z] (f : (i : ι) → C(Z × X i, Y)) (g : C(Z, Y)) (hf : ∀ (i : ι) (z : Z), (f i) (z, x i) = g z) : C(Z × WedgeSum x, Y)

Maps out of Z × ⋁ᵢ Xᵢ. For a locally compact space Z, maps Z × X i → Y which agree on Z × {x i} with a common map Z → Y assemble into a map out of the product of Z with the wedge sum. For Z = I this builds homotopies out of a wedge sum from homotopies of the summands which keep the base points together.

Equations

• TauCeti.WedgeSum.liftProd f g hf = (TauCeti.WedgeSum.lift (fun (i : ι) => ((f i).comp ContinuousMap.prodSwap).curry) g ⋯).uncurry.comp ContinuousMap.prodSwap

@[simp]

theorem TauCeti.WedgeSum.liftProd_incl {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] {Z : Type u_1} [TopologicalSpace Z] [LocallyCompactSpace Z] (f : (i : ι) → C(Z × X i, Y)) (g : C(Z, Y)) (hf : ∀ (i : ι) (z : Z), (f i) (z, x i) = g z) (z : Z) (i : ι) (a : X i) : (liftProd f g hf) (z, (incl x i) a) = (f i) (z, a)

@[simp]

theorem TauCeti.WedgeSum.liftProd_base {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {Y : Type w} [TopologicalSpace Y] {Z : Type u_1} [TopologicalSpace Z] [LocallyCompactSpace Z] (f : (i : ι) → C(Z × X i, Y)) (g : C(Z, Y)) (hf : ∀ (i : ι) (z : Z), (f i) (z, x i) = g z) (z : Z) : (liftProd f g hf) (z, base x) = g z

noncomputable def TauCeti.WedgeSum.subtypeVal {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) : C(WedgeSum fun (i : ι) => ⟨x i, ⋯⟩, WedgeSum x)

The map from the wedge sum of subsets S i ∋ x i of the summands into the wedge sum of the summands, induced by the inclusions.

Equations

• TauCeti.WedgeSum.subtypeVal hS = TauCeti.WedgeSum.lift (fun (i : ι) => (TauCeti.WedgeSum.incl x i).comp (ContinuousMap.subtypeVal (S i))) (TauCeti.WedgeSum.base x) ⋯

@[simp]

theorem TauCeti.WedgeSum.subtypeVal_incl {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) (i : ι) (a : ↑(S i)) : (subtypeVal hS) ((incl (fun (i : ι) => ⟨x i, ⋯⟩) i) a) = (incl x i) ↑a

@[simp]

theorem TauCeti.WedgeSum.subtypeVal_base {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) : (subtypeVal hS) (base fun (i : ι) => ⟨x i, ⋯⟩) = base x

theorem TauCeti.WedgeSum.incl_mem_range_subtypeVal_iff {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) {i : ι} {z : X i} : (incl x i) z ∈ Set.range ⇑(subtypeVal hS) ↔ z ∈ S i

A point of a summand lies in the image of the wedge sum of the subsets S i ∋ x i exactly when it lies in S i.

theorem TauCeti.WedgeSum.base_mem_range_subtypeVal {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) : base x ∈ Set.range ⇑(subtypeVal hS)

theorem TauCeti.WedgeSum.subtypeVal_injective {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) : Function.Injective ⇑(subtypeVal hS)

theorem TauCeti.WedgeSum.isOpenEmbedding_subtypeVal {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {S : (i : ι) → Set (X i)} (hS : ∀ (i : ι), x i ∈ S i) (hSo : ∀ (i : ι), IsOpen (S i)) : Topology.IsOpenEmbedding ⇑(subtypeVal hS)

A wedge of open neighbourhoods is an open subspace. For open subsets S i ∋ x i of the summands, the wedge sum of the S i maps homeomorphically onto an open subset of the wedge sum of the X i.

noncomputable def TauCeti.WedgeSum.proj {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] (x : (i : ι) → X i) (i : ι) : C(WedgeSum x, X i)

The retraction of the wedge sum onto its i-th summand, collapsing every other summand to the base point x i.

Equations

• TauCeti.WedgeSum.proj x i = TauCeti.WedgeSum.lift (fun (j : ι) => if h : j = i then h ▸ ContinuousMap.id (X j) else ContinuousMap.const (X j) (x i)) (x i) ⋯

@[simp]

theorem TauCeti.WedgeSum.proj_incl_self {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} (i : ι) (z : X i) : (proj x i) ((incl x i) z) = z

@[simp]

theorem TauCeti.WedgeSum.proj_incl_of_ne {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} {i j : ι} (h : j ≠ i) (z : X j) : (proj x i) ((incl x j) z) = x i

@[simp]

theorem TauCeti.WedgeSum.proj_base {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} (i : ι) : (proj x i) (base x) = x i

@[simp]

theorem TauCeti.WedgeSum.proj_comp_incl {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] {x : (i : ι) → X i} (i : ι) : (proj x i).comp (incl x i) = ContinuousMap.id (X i)

The retraction onto a summand is a left inverse of its inclusion.