Grace/Cumulus/Topology/Maps.g17

Open in Workbench Download source

Imports

CompactMore · CompactImage

Declarations

Source

1-- Continuous maps: constant maps, inclusions, restrictions and2-- corestrictions, closed sets of a closed subspace, the pasting lemma,3-- open and closed maps, homeomorphisms as an equivalence, and a4-- continuous bijection from a compact space onto a Hausdorff space as a5-- homeomorphism6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Topology.Maps12import CompactMore13import CompactImage1415-- Constant maps and inclusions are continuous.1617theorem ContinuousMap.constant (X T Y S y : Set)18  requires topology : IsTopology(X, T)19  requires hy : y ∈ Y20  shows ContinuousMap(constantFunction(X, Y, y), X, T, Y, S)21proof22  have function := constantFunction.function at X, Y, y with hy23  constructor24  . exact function25  . intros V hV26    have split : y ∈ V ∨ ¬y ∈ V by tauto27    cases split with inV | outside28    . have equal : functionPreimage(constantFunction(X, Y, y), X, V) = X29        apply Subset.antisymmetric30        . exact functionPreimage.subset at constantFunction(X, Y, y), X, V31        . intros x hx32          have value := constantFunction.apply with hx, hy33          apply functionPreimage.membership.backward34          rw value35          exact ⟨hx, inV⟩36      rw equal37      exact IsTopology.whole with topology38    . have equal : functionPreimage(constantFunction(X, Y, y), X, V) = ∅39        apply Subset.empty_iff.forward40        intros x hx41        have parts := functionPreimage.membership.forward with hx42        have value := constantFunction.apply with parts.left, hy43        rw value at parts44        exfalso45        exact outside with parts.right46      rw equal47      exact IsTopology.empty with topology4849theorem ContinuousMap.inclusion (X T A : Set)50  requires topology : IsTopology(X, T)51  requires hA : A ⊆ X52  shows ContinuousMap(inclusionMap(A, X), A, subspaceTopology(T, A), X, T)53proof54  have function := inclusionMap.function at A, X with hA55  constructor56  . exact function57  . intros V hV58    have equal : functionPreimage(inclusionMap(A, X), A, V) = V ∩ A59      ext x60      constructor61      . intro hx62        have parts := functionPreimage.membership.forward with hx63        have value := inclusionMap.value at A, X, x with hA, parts.left64        rw value at parts65        exact intersection.membership.backward with ⟨parts.right, parts.left⟩66      . intro hx67        have parts := intersection.membership.forward with hx68        have value := inclusionMap.value at A, X, x with hA, parts.right69        apply functionPreimage.membership.backward70        rw value71        exact ⟨parts.right, parts.left⟩72    rw equal73    exact subspaceTopology.membership.backward with ⟨V, hV, rfl⟩7475-- Restriction to a subspace and corestriction to a subspace of the76-- codomain.7778theorem restrict.preimage (f X Y A V : Set)79  requires function : f : X → Y80  requires hA : A ⊆ X81  shows functionPreimage(restrict(f, A), A, V) = functionPreimage(f, X, V) ∩ A82proof83  ext x84  constructor85  . intro hx86    have parts := functionPreimage.membership.forward with hx87    have value := restrict.domain_apply with function, hA, parts.left88    rw value at parts89    have hxX := hA with x, parts.left90    exact intersection.membership.backward with ⟨(functionPreimage.membership.backward with ⟨hxX, parts.right⟩), parts.left⟩91  . intro hx92    have parts := intersection.membership.forward with hx93    have inner := functionPreimage.membership.forward with parts.left94    have value := restrict.domain_apply with function, hA, parts.right95    apply functionPreimage.membership.backward96    rw value97    exact ⟨parts.right, inner.right⟩9899theorem ContinuousMap.restrict (f X T Y S A : Set)100  requires continuous : ContinuousMap(f, X, T, Y, S)101  requires hA : A ⊆ X102  shows ContinuousMap(restrict(f, A), A, subspaceTopology(T, A), Y, S)103proof104  have function := continuous.left105  constructor106  . exact restrict.domain_function with function, hA107  . intros V hV108    have equal := restrict.preimage at f, X, Y, A, V with function, hA109    rw equal110    have isOpen := continuous.right with V, hV111    exact subspaceTopology.membership.backward with ⟨functionPreimage(f, X, V), isOpen, rfl⟩112113theorem ContinuousMap.corestrict (f X T Y S B : Set)114  requires continuous : ContinuousMap(f, X, T, Y, S)115  requires hB : B ⊆ Y116  requires values : ∀ x ∈ X, f(x) ∈ B117  shows ContinuousMap(f, X, T, B, subspaceTopology(S, B))118proof119  have function := continuous.left120  constructor121  . exact FunctionBetween.codomain_of_values with function, values122  . intros W hW123    obtain ⟨V, hV, shape⟩ := subspaceTopology.membership.forward with hW124    have equal : functionPreimage(f, X, W) = functionPreimage(f, X, V)125      ext x126      constructor127      . intro hx128        have parts := functionPreimage.membership.forward with hx129        rw ← shape at parts130        have inner := intersection.membership.forward with parts.right131        exact functionPreimage.membership.backward with ⟨parts.left, inner.left⟩132      . intro hx133        have parts := functionPreimage.membership.forward with hx134        apply functionPreimage.membership.backward135        refine ⟨parts.left, ?_⟩136        rw ← shape137        exact intersection.membership.backward with ⟨parts.right, (values with x, parts.left)⟩138    rw equal139    exact continuous.right with V, hV140141theorem ContinuousMap.into_image (f X T Y S : Set)142  requires continuous : ContinuousMap(f, X, T, Y, S)143  shows ContinuousMap(f, X, T, functionImage(f, X, Y), subspaceTopology(S, functionImage(f, X, Y)))144proof145  have function := continuous.left146  apply ContinuousMap.corestrict with continuous, (functionImage.subset at f, X, Y)147  intros x hx148  exact functionImage.value with function, hx149150-- Closed sets of a subspace: traces of closed sets, and closed sets of a151-- closed subspace are closed in the whole space.152153theorem IsClosed.subspace_trace (X T A C : Set)154  requires topology : IsTopology(X, T)155  requires hA : A ⊆ X156  requires closed : IsClosed(X, T, C)157  shows IsClosed(A, subspaceTopology(T, A), C ∩ A)158proof159  constructor160  . exact intersection.subset_right at C, A161  . have equal : complement(A, C ∩ A) = complement(X, C) ∩ A162      ext x163      constructor164      . intro hx165        have parts := complement.membership.forward with hx166        have hxX := hA with x, parts.left167        apply intersection.membership.backward168        refine ⟨?_, parts.left⟩169        apply complement.membership.backward170        refine ⟨hxX, ?_⟩171        intro inC172        apply parts.right173        exact intersection.membership.backward with ⟨inC, parts.left⟩174      . intro hx175        have parts := intersection.membership.forward with hx176        have away := complement.membership.forward with parts.left177        apply complement.membership.backward178        refine ⟨parts.right, ?_⟩179        intro inBoth180        have inner := intersection.membership.forward with inBoth181        exact away.right with inner.left182    rw equal183    exact subspaceTopology.membership.backward with ⟨complement(X, C), closed.right, rfl⟩184185theorem IsClosed.of_closed_subspace (X T A C : Set)186  requires topology : IsTopology(X, T)187  requires closedA : IsClosed(X, T, A)188  requires closed : IsClosed(A, subspaceTopology(T, A), C)189  shows IsClosed(X, T, C)190proof191  have hA := closedA.left192  have hCA := closed.left193  obtain ⟨U, hU, shape⟩ := subspaceTopology.membership.forward with closed.right194  have equal : C = A ∩ complement(X, U)195    ext x196    constructor197    . intro hx198      have hxA := hCA with x, hx199      apply intersection.membership.backward200      refine ⟨hxA, ?_⟩201      apply complement.membership.backward202      refine ⟨(hA with x, hxA), ?_⟩203      intro inU204      have inTrace : x ∈ U ∩ A := intersection.membership.backward with ⟨inU, hxA⟩205      rw shape at inTrace206      have away := complement.membership.forward with inTrace207      exact away.right with hx208    . intro hx209      have parts := intersection.membership.forward with hx210      have away := complement.membership.forward with parts.right211      by_contra outside212      have inComplement : x ∈ complement(A, C) := complement.membership.backward with ⟨parts.left, outside⟩213      rw ← shape at inComplement214      have inner := intersection.membership.forward with inComplement215      exact away.right with inner.left216  rw equal217  exact IsClosed.intersection2 with topology, closedA, (Open.complement_closed with topology, hU)218219-- The pasting lemma: a map continuous on each of two closed pieces220-- covering the space is continuous.221theorem ContinuousMap.pasting (f X T Y S C D : Set)222  requires topologyX : IsTopology(X, T)223  requires topologyY : IsTopology(Y, S)224  requires function : f : X → Y225  requires closedC : IsClosed(X, T, C)226  requires closedD : IsClosed(X, T, D)227  requires whole : C ∪ D = X228  requires onC : ContinuousMap(restrict(f, C), C, subspaceTopology(T, C), Y, S)229  requires onD : ContinuousMap(restrict(f, D), D, subspaceTopology(T, D), Y, S)230  shows ContinuousMap(f, X, T, Y, S)231proof232  have hC := closedC.left233  have hD := closedD.left234  apply ContinuousMap.of_closed_preimages with topologyX, topologyY, function235  intros K closedK236  have preimageC := ContinuousMap.closed_preimage with onC, closedK237  have preimageD := ContinuousMap.closed_preimage with onD, closedK238  have equalC := restrict.preimage at f, X, Y, C, K with function, hC239  have equalD := restrict.preimage at f, X, Y, D, K with function, hD240  rw equalC at preimageC241  rw equalD at preimageD242  have closedInC := IsClosed.of_closed_subspace with topologyX, closedC,243    preimageC244  have closedInD := IsClosed.of_closed_subspace with topologyX, closedD,245    preimageD246  have below := functionPreimage.subset at f, X, K247  have split : functionPreimage(f, X, K) = functionPreimage(f, X, K) ∩ C ∪ functionPreimage(f, X, K) ∩ D248    rw [← intersection.union2_distrib, whole]249    symm250    exact intersection.eq_left_of_subset with below251  rw split252  exact IsClosed.union2 with topologyX, closedInC, closedInD253254-- Open maps, closed maps, and homeomorphisms.255256predicate OpenMap (f X T Y S : Set) :=257  FunctionBetween(f, X, Y) ∧ (∀ U ∈ T, functionImage(f, U, Y) ∈ S)258259predicate ClosedMap (f X T Y S : Set) :=260  FunctionBetween(f, X, Y) ∧261  (∀ C, IsClosed(X, T, C) → IsClosed(Y, S, functionImage(f, C, Y)))262263-- Under a bijection the image of U is the preimage of U under the inverse.264theorem Bijective.image_eq_preimage (f X Y U : Set)265  requires bijective : BijectiveBetween(f, X, Y)266  requires hU : U ⊆ X267  shows functionImage(f, U, Y) = functionPreimage(converse(f, X, Y), Y, U)268proof269  ext y270  constructor271  . intro hy272    have parts := functionImage.membership.forward with hy273    obtain ⟨hyY, x, hx, shape⟩ := parts274    have back := Bijective.inverse_apply with bijective, (hU with x, hx)275    have back2 : converse(f, X, Y)(y) = x276      rw shape277      exact back278    apply functionPreimage.membership.backward279    rw back2280    exact ⟨hyY, hx⟩281  . intro hy282    have parts := functionPreimage.membership.forward with hy283    have forward := Bijective.apply_inverse with bijective, parts.left284    apply functionImage.membership.backward285    refine ⟨parts.left, converse(f, X, Y)(y), parts.right, ?_⟩286    rw forward287    rfl288289theorem IsHomeomorphism.open_map (f X T Y S : Set)290  requires topology : IsTopology(X, T)291  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)292  shows OpenMap(f, X, T, Y, S)293proof294  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism295  constructor296  . exact continuous.left297  . intros U hU298    have equal := Bijective.image_eq_preimage with bijective, (IsTopology.subset with topology, hU)299    rw equal300    exact inverse.right with U, hU301302theorem IsHomeomorphism.closed_map (f X T Y S : Set)303  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)304  shows ClosedMap(f, X, T, Y, S)305proof306  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism307  constructor308  . exact continuous.left309  . intros C closed310    have equal := Bijective.image_eq_preimage with bijective, closed.left311    rw equal312    exact ContinuousMap.closed_preimage with inverse, closed313314theorem IsHomeomorphism.of_open_bijection (f X T Y S : Set)315  requires topology : IsTopology(X, T)316  requires bijective : BijectiveBetween(f, X, Y)317  requires continuous : ContinuousMap(f, X, T, Y, S)318  requires openMap : OpenMap(f, X, T, Y, S)319  shows IsHomeomorphism(f, X, T, Y, S)320proof321  refine ⟨bijective, continuous, ?_⟩322  constructor323  . exact converse.function_of_bijective with bijective324  . intros U hU325    have equal := Bijective.image_eq_preimage with bijective, (IsTopology.subset with topology, hU)326    rw ← equal327    exact openMap.right with U, hU328329theorem IsHomeomorphism.of_closed_bijection (f X T Y S : Set)330  requires topologyX : IsTopology(X, T)331  requires topologyY : IsTopology(Y, S)332  requires bijective : BijectiveBetween(f, X, Y)333  requires continuous : ContinuousMap(f, X, T, Y, S)334  requires closedMap : ClosedMap(f, X, T, Y, S)335  shows IsHomeomorphism(f, X, T, Y, S)336proof337  refine ⟨bijective, continuous, ?_⟩338  have inverse := converse.function_of_bijective with bijective339  apply ContinuousMap.of_closed_preimages with topologyY, topologyX, inverse340  intros C closed341  have equal := Bijective.image_eq_preimage with bijective, closed.left342  rw ← equal343  exact closedMap.right with C, closed344345theorem IsHomeomorphism.identity (X T : Set)346  requires topology : IsTopology(X, T)347  shows IsHomeomorphism(identity(X), X, T, X, T)348proof349  have openMap : OpenMap(identity(X), X, T, X, T)350    constructor351    . exact identity.function at X352    . intros U hU353      have equal := functionImage.identity_of_subset with (IsTopology.subset with topology, hU)354      rwa equal355  exact IsHomeomorphism.of_open_bijection with topology, (identity.bijective at X), (ContinuousMap.identity with topology), openMap356357theorem OpenMap.compose (g f X T Y S Z R : Set)358  requires topology : IsTopology(X, T)359  requires first : OpenMap(f, X, T, Y, S)360  requires second : OpenMap(g, Y, S, Z, R)361  shows OpenMap(compose(g, f, X, Y, Z), X, T, Z, R)362proof363  have fFunction := first.left364  have gFunction := second.left365  constructor366  . exact compose.function with fFunction, gFunction367  . intros U hU368    have hUX := IsTopology.subset with topology, hU369    have equal := functionImage.compose with fFunction, gFunction, hUX370    rw equal371    exact second.right with functionImage(f, U, Y), (first.right with U, hU)372373theorem ClosedMap.compose (g f X T Y S Z R : Set)374  requires first : ClosedMap(f, X, T, Y, S)375  requires second : ClosedMap(g, Y, S, Z, R)376  shows ClosedMap(compose(g, f, X, Y, Z), X, T, Z, R)377proof378  have fFunction := first.left379  have gFunction := second.left380  constructor381  . exact compose.function with fFunction, gFunction382  . intros C closed383    have equal := functionImage.compose with fFunction, gFunction, closed.left384    rw equal385    exact second.right with functionImage(f, C, Y), (first.right with C, closed)386387theorem IsHomeomorphism.compose (g f X T Y S Z R : Set)388  requires topologyX : IsTopology(X, T)389  requires topologyY : IsTopology(Y, S)390  requires first : IsHomeomorphism(f, X, T, Y, S)391  requires second : IsHomeomorphism(g, Y, S, Z, R)392  shows IsHomeomorphism(compose(g, f, X, Y, Z), X, T, Z, R)393proof394  have openF := IsHomeomorphism.open_map with topologyX, first395  have openG := IsHomeomorphism.open_map with topologyY, second396  have openMap := OpenMap.compose with topologyX, openF, openG397  obtain ⟨bijectiveF, continuousF, inverseF⟩ := first398  obtain ⟨bijectiveG, continuousG, inverseG⟩ := second399  have bijective := compose.bijective with bijectiveF, bijectiveG400  have continuous := ContinuousMap.compose with continuousF, continuousG401  exact IsHomeomorphism.of_open_bijection with topologyX, bijective, continuous, openMap402403-- A continuous map from a compact space to a Hausdorff space is closed,404-- so a continuous bijection between them is a homeomorphism.405406theorem IsCompact.continuous_closed_map (f X T Y S : Set)407  requires topologyX : IsTopology(X, T)408  requires topologyY : IsTopology(Y, S)409  requires compact : IsCompact(X, T, X)410  requires hausdorff : IsHausdorff(Y, S)411  requires continuous : ContinuousMap(f, X, T, Y, S)412  shows ClosedMap(f, X, T, Y, S)413proof414  constructor415  . exact continuous.left416  . intros C closed417    have compactC := IsCompact.closed_subset with topologyX, compact, closed, closed.left418    have compactImage := IsCompact.image with continuous, compactC419    exact IsCompact.hausdorff_closed with topologyY, hausdorff, compactImage420421theorem IsHomeomorphism.compact_hausdorff (f X T Y S : Set)422  requires topologyX : IsTopology(X, T)423  requires topologyY : IsTopology(Y, S)424  requires compact : IsCompact(X, T, X)425  requires hausdorff : IsHausdorff(Y, S)426  requires bijective : BijectiveBetween(f, X, Y)427  requires continuous : ContinuousMap(f, X, T, Y, S)428  shows IsHomeomorphism(f, X, T, Y, S)429proof430  have closedMap := IsCompact.continuous_closed_map with topologyX, topologyY, compact, hausdorff, continuous431  exact IsHomeomorphism.of_closed_bijection with topologyX, topologyY, bijective, continuous, closedMap432433-- Topological properties carried along maps.434435theorem IsCompact.of_surjection (f X T Y S : Set)436  requires continuous : ContinuousMap(f, X, T, Y, S)437  requires surjective : SurjectiveBetween(f, X, Y)438  requires compact : IsCompact(X, T, X)439  shows IsCompact(Y, S, Y)440proof441  have function := continuous.left442  have image := IsCompact.image with continuous, compact443  have whole : functionImage(f, X, Y) = Y444    apply Subset.antisymmetric445    . exact functionImage.subset at f, X, Y446    . intros y hy447      obtain ⟨x, hx, edge⟩ := surjective.right with y, hy448      have value := FunctionBetween.apply_value with function, hx, edge449      rw ← value450      exact functionImage.value with function, hx451  rwa whole at image452453theorem IsDense.image (f X T Y S A : Set)454  requires topologyX : IsTopology(X, T)455  requires topologyY : IsTopology(Y, S)456  requires continuous : ContinuousMap(f, X, T, Y, S)457  requires surjective : SurjectiveBetween(f, X, Y)458  requires hA : A ⊆ X459  requires dense : IsDense(X, T, A)460  shows IsDense(Y, S, functionImage(f, A, Y))461proof462  have function := continuous.left463  have equal : closure(X, T, A) = X := dense464  have inclusion := ContinuousMap.image_closure with topologyX, topologyY, continuous, hA465  rw equal at inclusion466  have whole : functionImage(f, X, Y) = Y467    apply Subset.antisymmetric468    . exact functionImage.subset at f, X, Y469    . intros y hy470      obtain ⟨x, hx, edge⟩ := surjective.right with y, hy471      have value := FunctionBetween.apply_value with function, hx, edge472      rw ← value473      exact functionImage.value with function, hx474  rw whole at inclusion475  have inside := closure.subset with topologyY, (functionImage.subset at f, A, Y)476  exact Subset.antisymmetric with inside, inclusion477478theorem IsHausdorff.of_homeomorphism (f X T Y S : Set)479  requires topologyX : IsTopology(X, T)480  requires topologyY : IsTopology(Y, S)481  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)482  requires hausdorff : IsHausdorff(X, T)483  shows IsHausdorff(Y, S)484proof485  have openMap := IsHomeomorphism.open_map with topologyX, homeomorphism486  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism487  have injective := Bijective.injective with bijective488  have inverseFunction := converse.function_of_bijective with bijective489  intros y1 hy1 y2 hy2 distinct490  have hx1 := FunctionBetween.apply_closed with inverseFunction, hy1491  have hx2 := FunctionBetween.apply_closed with inverseFunction, hy2492  have forward1 := Bijective.apply_inverse with bijective, hy1493  have forward2 := Bijective.apply_inverse with bijective, hy2494  have distinctX : converse(f, X, Y)(y1) ≠ converse(f, X, Y)(y2)495    intro same496    apply distinct497    rw [← forward1, ← forward2, same]498    rfl499  obtain ⟨U, hU, V, hV, inU, inV, disjoint⟩ := hausdorff with converse(f, X, Y)(y1), hx1, converse(f, X, Y)(y2), hx2, distinctX500  have separated := Disjoint.iff.forward with disjoint501  have hUX := IsTopology.subset with topologyX, hU502  have hVX := IsTopology.subset with topologyX, hV503  refine ⟨functionImage(f, U, Y), (openMap.right with U, hU), functionImage(f, V, Y), (openMap.right with V, hV), ?_, ?_, ?_⟩504  . apply functionImage.membership.backward505    refine ⟨hy1, converse(f, X, Y)(y1), inU, ?_⟩506    rw forward1507    rfl508  . apply functionImage.membership.backward509    refine ⟨hy2, converse(f, X, Y)(y2), inV, ?_⟩510    rw forward2511    rfl512  . apply Disjoint.iff.backward513    intros z hzU hzV514    have partsU := functionImage.membership.forward with hzU515    have partsV := functionImage.membership.forward with hzV516    obtain ⟨hzY, a, ha, shapeA⟩ := partsU517    obtain ⟨hzY2, b, hb, shapeB⟩ := partsV518    have same : f(a) = f(b)519      rw [← shapeA, ← shapeB]520      rfl521    have equal := Injective.apply_cancel with injective, (hUX with a, ha), (hVX with b, hb), same522    rw equal at ha523    exact separated with b, ha, hb524