Grace/Cumulus/Set/Function/Projection.g17

Open in Workbench Download source

Imports

Image

Declarations

Source

1-- Coordinate projections of a product: the first and second coordinate2-- of a pair as functions on A × B, bijective when the other factor is a3-- point4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Set.Function.Projection10import Image1112-- Coordinates of a pair, as functions on the product.13defunique firstOf (A B p : Set) (x ∈ A) := ∃ y ∈ B, p = (x, y)14requires pair : p ∈ A × B15proof16  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair17  refine ⟨x, hx, y, hy, shape⟩18uniqueness19  intros u hu first v hv second20  obtain ⟨b, hb, shapeU⟩ := first21  obtain ⟨d, hd, shapeV⟩ := second22  have equal : (u, b) = (v, d) by cc23  have coordinates := orderedPair.injective with equal24  exact coordinates.left2526defunique secondOf (A B p : Set) (y ∈ B) := ∃ x ∈ A, p = (x, y)27requires pair : p ∈ A × B28proof29  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with pair30  refine ⟨y, hy, x, hx, shape⟩31uniqueness32  intros u hu first v hv second33  obtain ⟨a, ha, shapeU⟩ := first34  obtain ⟨c, hc, shapeV⟩ := second35  have equal : (a, u) = (c, v) by cc36  have coordinates := orderedPair.injective with equal37  exact coordinates.right3839defgraph firstProjection (A B : Set) (p ∈ A × B) : A := firstOf(A, B, p)40proof41  have selected := firstOf.selected with member42  exact selected.left4344defgraph secondProjection (A B : Set) (p ∈ A × B) : B := secondOf(A, B, p)45proof46  have selected := secondOf.selected with member47  exact selected.left4849theorem firstProjection.pair (A B x y : Set)50  requires hx : x ∈ A51  requires hy : y ∈ B52  shows firstProjection(A, B)((x, y)) = x53proof54  have pair := product.pair at x, y, A, B with *55  have selected := firstOf.selected with pair56  obtain ⟨b, hb, shape⟩ := selected.right57  have coordinates := orderedPair.injective with shape58  have value := firstProjection.value with pair59  cc6061theorem secondProjection.pair (A B x y : Set)62  requires hx : x ∈ A63  requires hy : y ∈ B64  shows secondProjection(A, B)((x, y)) = y65proof66  have pair := product.pair at x, y, A, B with *67  have selected := secondOf.selected with pair68  obtain ⟨a, ha, shape⟩ := selected.right69  have coordinates := orderedPair.injective with shape70  have value := secondProjection.value with pair71  cc7273-- Over a single point in the other factor, a projection is a bijection.74theorem firstProjection.bijective_singleton (A b : Set)75  shows BijectiveBetween(firstProjection(A, {b}), A × {b}, A)76proof77  have function := firstProjection.function at A, {b}78  have self : b ∈ {b} by simp [singleton.membership]79  constructor80  . constructor81    . exact function82    . intros p hp q hq z hz hpz hqz83      have valueP := FunctionBetween.apply_value with function, hp, hpz84      have valueQ := FunctionBetween.apply_value with function, hq, hqz85      obtain ⟨boundP, x, hx, y, hy, shapeP⟩ := product.membership.forward with hp86      obtain ⟨boundQ, u, hu, v, hv, shapeQ⟩ := product.membership.forward with hq87      have sameY := singleton.membership.forward with hy88      have sameV := singleton.membership.forward with hv89      rw shapeP at valueP90      rw shapeQ at valueQ91      have pairP := firstProjection.pair with hx, hy92      have pairQ := firstProjection.pair with hu, hv93      rw [shapeP, shapeQ, sameY, sameV]94      have equal : x = u by cc95      rw equal96      rfl97  . constructor98    . exact function99    . intros x hx100      have pair := product.pair with hx, self101      refine ⟨(x, b), pair, ?_⟩102      have value := firstProjection.pair with hx, self103      have related := FunctionBetween.relates_apply with function, pair104      rwa value at related105106theorem secondProjection.bijective_singleton (a B : Set)107  shows BijectiveBetween(secondProjection({a}, B), {a} × B, B)108proof109  have function := secondProjection.function at {a}, B110  have self : a ∈ {a} by simp [singleton.membership]111  constructor112  . constructor113    . exact function114    . intros p hp q hq z hz hpz hqz115      have valueP := FunctionBetween.apply_value with function, hp, hpz116      have valueQ := FunctionBetween.apply_value with function, hq, hqz117      obtain ⟨boundP, x, hx, y, hy, shapeP⟩ := product.membership.forward with hp118      obtain ⟨boundQ, u, hu, v, hv, shapeQ⟩ := product.membership.forward with hq119      have sameX := singleton.membership.forward with hx120      have sameU := singleton.membership.forward with hu121      rw shapeP at valueP122      rw shapeQ at valueQ123      have pairP := secondProjection.pair with hx, hy124      have pairQ := secondProjection.pair with hu, hv125      rw [shapeP, shapeQ, sameX, sameU]126      have equal : y = v by cc127      rw equal128      rfl129  . constructor130    . exact function131    . intros y hy132      have pair := product.pair with self, hy133      refine ⟨(a, y), pair, ?_⟩134      have value := secondProjection.pair with self, hy135      have related := FunctionBetween.relates_apply with function, pair136      rwa value at related137