Grace/Cumulus/Relation/QuotientMap.g17

Open in Workbench Download source

Imports

QuotientOperations

Declarations

Source

1-- Descent of functions through equivalence quotients, entirely in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Relation.QuotientMap8import QuotientOperations910predicate Respects (f A r : Set) :=11  ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → f(x) = f(y)1213defunique quotientMapValue (f A B r X : Set) (y ∈ B) :=14  ∃ x ∈ A, X = ⟦x⟧[A, r] ∧ y = f(x)15requires function : f : A → B16requires equivalence : Equivalence(A, r)17requires respects : Respects(f, A, r)18requires member : X ∈ (A ⧸ r)19proof20  obtain ⟨x, hx, shape⟩ := quotient.representative at A, r, X with member21  have valueIn := FunctionBetween.apply_closed at f, A, B, x with *22  refine ⟨f(x), valueIn, x, hx, shape, rfl⟩23uniqueness24  intros y hy py z hz pz25  obtain ⟨x, hx, sx, vx⟩ := py26  obtain ⟨u, hu, su, vu⟩ := pz27  have equal : ⟦x⟧[A, r] = ⟦u⟧[A, r]28    cc29  have related := equivalenceClass.related_of_eq at A, r, x, u with *30  unfold Respects at respects31  have images := respects with x, hx, u, hu, related32  cc3334defgraph quotientMap (f A B r : Set) (X ∈ (A ⧸ r)) : B := quotientMapValue(f, A, B, r, X)35requires function : f : A → B36requires equivalence : Equivalence(A, r)37requires respects : Respects(f, A, r)38proof39  have selected := quotientMapValue.selected at f, A, B, r, X with *40  exact selected.left4142theorem quotientMap.class (f A B r x : Set)43  requires function : f : A → B44  requires equivalence : Equivalence(A, r)45  requires respects : Respects(f, A, r)46  requires hx : x ∈ A47  shows quotientMap(f, A, B, r)(⟦x⟧[A, r]) = f(x)48proof49  have member := quotient.contains_class with *50  have value := quotientMap.value at f, A, B, r, ⟦x⟧[A, r] with *51  have selected := quotientMapValue.selected at f, A, B, r, ⟦x⟧[A, r] with *52  obtain ⟨u, hu, shape, output⟩ := selected.right53  have related := equivalenceClass.related_of_eq with *54  have images := respects with x, hx, u, hu, related55  cc5657theorem quotientMap.injective (f A B r : Set)58  requires function : f : A → B59  requires equivalence : Equivalence(A, r)60  requires respects : Respects(f, A, r)61  requires reflects : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → relates(r, x, y)62  shows InjectiveBetween(quotientMap(f, A, B, r), (A ⧸ r), B)63proof64  have mapped := quotientMap.function at f, A, B, r with *65  unfold InjectiveBetween66  refine ⟨mapped, ?_⟩67  intros X hX Y hY z hz left right68  obtain ⟨x, hx, sx⟩ := quotient.representative with hX69  obtain ⟨y, hy, sy⟩ := quotient.representative with hY70  have vx := quotientMap.class with hx71  have vy := quotientMap.class with hy72  have ex := FunctionBetween.apply_value at quotientMap(f, A, B, r), (A ⧸ r), B, X, z with *73  have ey := FunctionBetween.apply_value at quotientMap(f, A, B, r), (A ⧸ r), B, Y, z with *74  have images : f(x) = f(y) by cc75  have related := reflects with x, hx, y, hy, images76  have classes := equivalenceClass.eq with *77  cc7879theorem quotientMap.surjective (f A B r : Set)80  requires function : f : A → B81  requires equivalence : Equivalence(A, r)82  requires respects : Respects(f, A, r)83  requires onto : SurjectiveBetween(f, A, B)84  shows SurjectiveBetween(quotientMap(f, A, B, r), (A ⧸ r), B)85proof86  have mapped := quotientMap.function at f, A, B, r with *87  unfold SurjectiveBetween88  refine ⟨mapped, ?_⟩89  intros y hy90  obtain ⟨x, hx, edge⟩ := onto.right with y, hy91  have member := quotient.contains_class with *92  have value := quotientMap.class with *93  have original := FunctionBetween.apply_value with *94  have image := FunctionBetween.relates_apply at quotientMap(f, A, B, r), (A ⧸ r), B, ⟦x⟧[A, r] with *95  refine ⟨⟦x⟧[A, r], member, ?_⟩96  cc9798-- The factorization equation determines the descended function uniquely.99theorem quotientMap.unique (f g A B r : Set)100  requires function : f : A → B101  requires equivalence : Equivalence(A, r)102  requires respects : Respects(f, A, r)103  requires candidate : g : (A ⧸ r) → B104  requires factors : ∀ x ∈ A, g(⟦x⟧[A, r]) = f(x)105  shows g = quotientMap(f, A, B, r)106proof107  have mapped := quotientMap.function at f, A, B, r with *108  apply FunctionBetween.ext with candidate, mapped109  intros X hX110  obtain ⟨x, hx, shape⟩ := quotient.representative with hX111  have given := factors with x, hx112  have canonical := quotientMap.class with *113  cc114115theorem quotientMap.factorization (f A B r : Set)116  requires function : f : A → B117  requires equivalence : Equivalence(A, r)118  requires respects : Respects(f, A, r)119  shows compose(quotientMap(f, A, B, r), quotientProjection(A, r), A, (A ⧸ r), B) = f120proof121  have projection := quotientProjection.function at A, r with *122  have mapped := quotientMap.function at f, A, B, r with *123  have composed := compose.function at quotientMap(f, A, B, r), quotientProjection(A, r), A, (A ⧸ r), B with *124  apply FunctionBetween.ext with composed, function125  intros x hx126  have composition := compose.apply at quotientMap(f, A, B, r), quotientProjection(A, r), A, (A ⧸ r), B, x with *127  have projected := quotientProjection.value at A, r, x with *128  have evaluated := quotientMap.class with *129  cc130131theorem quotientMap.binary (f A B r op target X Y : Set)132  requires function : f : A → B133  requires equivalence : Equivalence(A, r)134  requires respects : Respects(f, A, r)135  requires closed : IsMagma(A, op)136  requires compatible : CompatibleBinary(A, r, op)137  requires preserves : ∀ x ∈ A, ∀ y ∈ A, f(op(x, y)) = target(f(x), f(y))138  requires hX : X ∈ (A ⧸ r)139  requires hY : Y ∈ (A ⧸ r)140  shows quotientMap(f, A, B, r)((quotientBinary(A, r, op))(X, Y)) =141    target(quotientMap(f, A, B, r)(X), quotientMap(f, A, B, r)(Y))142proof143  obtain ⟨x, hx, sx⟩ := quotient.representative with hX144  obtain ⟨y, hy, sy⟩ := quotient.representative with hY145  have operation := quotientBinary.classes at A, r, op, x, y with *146  have output := quotientMap.class at f, A, B, r, op(x, y) with *147  have vx := quotientMap.class at f, A, B, r, x with *148  have vy := quotientMap.class at f, A, B, r, y with *149  have original := preserves with x, hx, y, hy150  cc151152theorem quotientMap.unary (f A B r op target X : Set)153  requires function : f : A → B154  requires equivalence : Equivalence(A, r)155  requires respects : Respects(f, A, r)156  requires closed : op : A → A157  requires compatible : CompatibleUnary(A, r, op)158  requires preserves : ∀ x ∈ A, f(op(x)) = target(f(x))159  requires hX : X ∈ (A ⧸ r)160  shows quotientMap(f, A, B, r)((quotientUnary(A, r, op))(X)) =161    target(quotientMap(f, A, B, r)(X))162proof163  obtain ⟨x, hx, sx⟩ := quotient.representative with hX164  have operation := quotientUnary.classes at A, r, op, x with *165  have outputIn : op(x) ∈ A166    exact FunctionBetween.apply_closed at op, A, A, x with *167  have output := quotientMap.class at f, A, B, r, op(x) with *168  have vx := quotientMap.class at f, A, B, r, x with *169  have original := preserves with x, hx170  cc171