Grace/Cumulus/Relation/QuotientOperations.g17

Open in Workbench Download source

Imports

Quotient · Algebra.Ring.Core · Set.Function

Declarations

Source

1-- Choice-free lifting of compatible operations to quotient sets.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.QuotientOperations8import Quotient9import Algebra.Ring.Core10import Set.Function1112predicate CompatibleBinary (A r op : Set) :=13  ∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ A, ∀ v ∈ A,14    relates(r, x, y) → relates(r, u, v) → relates(r, op(x, u), op(y, v))15predicate CompatibleUnary (A r op : Set) :=16  ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, op(x), op(y))1718theorem quotient.representative (A r X : Set)19  requires member : X ∈ (A ⧸ r)20  shows ∃ x ∈ A, X = ⟦x⟧[A, r]21proof22  have data := quotient.membership.forward with member23  exact data.right2425-- The canonical quotient map exists without selecting representatives.26defgraph quotientProjection (A r : Set) (x ∈ A) : (A ⧸ r) := ⟦x⟧[A, r]27requires equivalence : Equivalence(A, r)28proof29  exact quotient.contains_class with *3031theorem quotientProjection.surjective (A r : Set)32  requires equivalence : Equivalence(A, r)33  shows SurjectiveBetween(quotientProjection(A, r), A, (A ⧸ r))34proof35  have function := quotientProjection.function at A, r with *36  unfold SurjectiveBetween37  refine ⟨function, ?_⟩38  intros X hX39  obtain ⟨x, hx, shape⟩ := quotient.representative with hX40  have value := quotientProjection.value at A, r, x with *41  have edge := FunctionBetween.relates_apply with *42  refine ⟨x, hx, ?_⟩43  rwa [shape, ← value]4445defunique quotientBinaryValue (A r op p : Set) (Z ∈ (A ⧸ r)) :=46  ∃ x ∈ A, ∃ y ∈ A, p = (⟦x⟧[A, r], ⟦y⟧[A, r]) ∧ Z = ⟦op(x, y)⟧[A, r]47requires equivalence : Equivalence(A, r)48requires closed : IsMagma(A, op)49requires compatible : CompatibleBinary(A, r, op)50requires pair : p ∈ (A ⧸ r) × (A ⧸ r)51proof52  obtain ⟨bounded, X, hX, Y, hY, shape⟩ := product.membership.forward with pair53  obtain ⟨x, hx, xClass⟩ := quotient.representative with hX54  obtain ⟨y, hy, yClass⟩ := quotient.representative with hY55  have valueIn := quotient.contains_class at A, r, op(x, y) with *56  have input : p = (⟦x⟧[A, r], ⟦y⟧[A, r]) by cc57  refine ⟨⟦op(x, y)⟧[A, r], valueIn, x, hx, y, hy, input, rfl⟩58uniqueness59  intros Z hZ propertyZ W hW propertyW60  obtain ⟨x, hx, y, hy, inputZ, outputZ⟩ := propertyZ61  obtain ⟨u, hu, v, hv, inputW, outputW⟩ := propertyW62  have inputs : (⟦x⟧[A, r], ⟦y⟧[A, r]) = (⟦u⟧[A, r], ⟦v⟧[A, r]) by cc63  have coordinates := orderedPair.injective with inputs64  have xu := equivalenceClass.related_of_eq with equivalence, hx, hu, coordinates.left65  have yv := equivalenceClass.related_of_eq with equivalence, hy, hv, coordinates.right66  have outputs := compatible with x, hx, u, hu, y, hy, v, hv, xu, yv67  have equal := equivalenceClass.eq at A, r, op(x, y), op(u, v) with *68  cc6970defgraph quotientBinary (A r op : Set) (p ∈ (A ⧸ r) × (A ⧸ r)) : (A ⧸ r) := quotientBinaryValue(A, r, op, p)71requires equivalence : Equivalence(A, r)72requires closed : IsMagma(A, op)73requires compatible : CompatibleBinary(A, r, op)74proof75  have selected := quotientBinaryValue.selected at A, r, op, p with *76  exact selected.left7778theorem quotientBinary.classes (A r op x y : Set)79  requires equivalence : Equivalence(A, r)80  requires closed : IsMagma(A, op)81  requires compatible : CompatibleBinary(A, r, op)82  requires hx : x ∈ A83  requires hy : y ∈ A84  shows (quotientBinary(A, r, op))(⟦x⟧[A, r], ⟦y⟧[A, r]) = ⟦op(x, y)⟧[A, r]85proof86  have xIn := quotient.contains_class at A, r, x with *87  have yIn := quotient.contains_class at A, r, y with *88  have pair := product.pair at ⟦x⟧[A, r], ⟦y⟧[A, r], (A ⧸ r), (A ⧸ r) with *89  have evaluated := quotientBinary.value at A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]) with *90  have selected := quotientBinaryValue.selected at A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]) with *91  obtain ⟨member, u, hu, v, hv, input, output⟩ := selected92  have coordinates := orderedPair.injective with input93  have xu := equivalenceClass.related_of_eq with equivalence, hx, hu, coordinates.left94  have yv := equivalenceClass.related_of_eq with equivalence, hy, hv, coordinates.right95  have related := compatible with x, hx, u, hu, y, hy, v, hv, xu, yv96  have equal := equivalenceClass.eq at A, r, op(x, y), op(u, v) with *97  have called : (quotientBinary(A, r, op))(⟦x⟧[A, r], ⟦y⟧[A, r]) = quotientBinaryValue(A, r, op, (⟦x⟧[A, r], ⟦y⟧[A, r]))98    unfold call299    cc100  cc101102defunique quotientUnaryValue (A r op X : Set) (Z ∈ (A ⧸ r)) :=103  ∃ x ∈ A, X = ⟦x⟧[A, r] ∧ Z = ⟦op(x)⟧[A, r]104requires equivalence : Equivalence(A, r)105requires closed : op : A → A106requires compatible : CompatibleUnary(A, r, op)107requires member : X ∈ (A ⧸ r)108proof109  obtain ⟨x, hx, shape⟩ := quotient.representative with member110  have valueInA : op(x) ∈ A111    exact FunctionBetween.apply_closed at op, A, A, x with *112  have valueIn := quotient.contains_class at A, r, op(x) with *113  refine ⟨⟦op(x)⟧[A, r], valueIn, x, hx, shape, rfl⟩114uniqueness115  intros Z hZ propertyZ W hW propertyW116  obtain ⟨x, hx, inputZ, outputZ⟩ := propertyZ117  obtain ⟨y, hy, inputW, outputW⟩ := propertyW118  have same : ⟦x⟧[A, r] = ⟦y⟧[A, r] by cc119  have xy := equivalenceClass.related_of_eq at A, r, x, y with *120  have outputs := compatible with x, hx, y, hy, xy121  have leftClosed : op(x) ∈ A122    exact FunctionBetween.apply_closed at op, A, A, x with *123  have rightClosed : op(y) ∈ A124    exact FunctionBetween.apply_closed at op, A, A, y with *125  have equal := equivalenceClass.eq at A, r, op(x), op(y) with *126  cc127128defgraph quotientUnary (A r op : Set) (X ∈ (A ⧸ r)) : (A ⧸ r) := quotientUnaryValue(A, r, op, X)129requires equivalence : Equivalence(A, r)130requires closed : op : A → A131requires compatible : CompatibleUnary(A, r, op)132proof133  have selected := quotientUnaryValue.selected at A, r, op, X with *134  exact selected.left135136theorem quotientUnary.classes (A r op x : Set)137  requires equivalence : Equivalence(A, r)138  requires closed : op : A → A139  requires compatible : CompatibleUnary(A, r, op)140  requires hx : x ∈ A141  shows (quotientUnary(A, r, op))(⟦x⟧[A, r]) = ⟦op(x)⟧[A, r]142proof143  have member := quotient.contains_class at A, r, x with *144  have evaluated := quotientUnary.value at A, r, op, ⟦x⟧[A, r] with *145  have selected := quotientUnaryValue.selected at A, r, op, ⟦x⟧[A, r] with *146  obtain ⟨bounded, y, hy, shape, output⟩ := selected147  have xy := equivalenceClass.related_of_eq at A, r, x, y with *148  have related := compatible with x, hx, y, hy, xy149  have leftClosed : op(x) ∈ A150    exact FunctionBetween.apply_closed at op, A, A, x with *151  have rightClosed : op(y) ∈ A152    exact FunctionBetween.apply_closed at op, A, A, y with *153  have equal := equivalenceClass.eq at A, r, op(x), op(y) with *154  have called : (quotientUnary(A, r, op))(⟦x⟧[A, r]) = quotientUnaryValue(A, r, op, ⟦x⟧[A, r])155    cc156  cc157158159theorem quotientBinary.magma (A r op : Set)160  requires equivalence : Equivalence(A, r)161  requires closed : IsMagma(A, op)162  requires compatible : CompatibleBinary(A, r, op)163  shows IsMagma((A ⧸ r), quotientBinary(A, r, op))164proof165  unfold IsMagma166  exact quotientBinary.function at A, r, op with *167168theorem quotientBinary.associative (A r op : Set)169  requires equivalence : Equivalence(A, r)170  requires closed : IsMagma(A, op)171  requires compatible : CompatibleBinary(A, r, op)172  requires law : Associative(A, op)173  shows Associative((A ⧸ r), quotientBinary(A, r, op))174proof175  intros X hX Y hY Z hZ176  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX177  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY178  obtain ⟨z, hz, zShape⟩ := quotient.representative with hZ179  rw [xShape, yShape, zShape]180  have xy := quotientBinary.classes at A, r, op, x, y with *181  have yz := quotientBinary.classes at A, r, op, y, z with *182  have lhs := quotientBinary.classes at A, r, op, op(x, y), z with *183  have rhs := quotientBinary.classes at A, r, op, x, op(y, z) with *184  have ordinary := law with x, hx, y, hy, z, hz185  cc186187theorem quotientBinary.commutative (A r op : Set)188  requires equivalence : Equivalence(A, r)189  requires closed : IsMagma(A, op)190  requires compatible : CompatibleBinary(A, r, op)191  requires law : Commutative(A, op)192  shows Commutative((A ⧸ r), quotientBinary(A, r, op))193proof194  intros X hX Y hY195  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX196  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY197  rw [xShape, yShape]198  have xy := quotientBinary.classes with hx, hy199  have yx := quotientBinary.classes with hy, hx200  have ordinary := law with x, hx, y, hy201  cc202203theorem quotientBinary.identity (A r op unit : Set)204  requires equivalence : Equivalence(A, r)205  requires closed : IsMagma(A, op)206  requires compatible : CompatibleBinary(A, r, op)207  requires law : Identity(A, op, unit)208  shows Identity((A ⧸ r), quotientBinary(A, r, op), ⟦unit⟧[A, r])209proof210  have unitIn := quotient.contains_class with equivalence, law.left211  unfold Identity212  refine ⟨unitIn, ?_⟩213  intros X hX214  obtain ⟨x, hx, shape⟩ := quotient.representative with hX215  rw shape216  have left := quotientBinary.classes with equivalence, closed, compatible, law.left, hx217  have right := quotientBinary.classes with equivalence, closed, compatible, hx, law.left218  have ordinary := law.right with x, hx219  have leftLaw := ordinary.left220  have rightLaw := ordinary.right221  constructor222  . cc223  . cc224225theorem quotientUnary.inverse (A r op unit inv : Set)226  requires equivalence : Equivalence(A, r)227  requires closed : IsMagma(A, op)228  requires compatible : CompatibleBinary(A, r, op)229  requires invCompatible : CompatibleUnary(A, r, inv)230  requires law : Inverse(A, op, unit, inv)231  shows Inverse((A ⧸ r), quotientBinary(A, r, op), ⟦unit⟧[A, r], quotientUnary(A, r, inv))232proof233  have invClosed := law.left234  have function := quotientUnary.function at A, r, inv with *235  unfold Inverse236  refine ⟨function, ?_⟩237  intros X hX238  obtain ⟨x, hx, shape⟩ := quotient.representative with hX239  rw shape240  have invIn : inv(x) ∈ A241    exact FunctionBetween.apply_closed with *242  have inverseValue := quotientUnary.classes with hx243  have left := quotientBinary.classes at A, r, op, inv(x), x with *244  have right := quotientBinary.classes at A, r, op, x, inv(x) with *245  have ordinary := law.right with x, hx246  have leftLaw := ordinary.left247  have rightLaw := ordinary.right248  constructor249  . cc250  . cc251252theorem quotientBinary.distributive (A r add mul : Set)253  requires equivalence : Equivalence(A, r)254  requires addClosed : IsMagma(A, add)255  requires mulClosed : IsMagma(A, mul)256  requires addCompatible : CompatibleBinary(A, r, add)257  requires mulCompatible : CompatibleBinary(A, r, mul)258  requires law : Distributive(A, add, mul)259  shows Distributive((A ⧸ r), quotientBinary(A, r, add), quotientBinary(A, r, mul))260proof261  intros X hX Y hY Z hZ262  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX263  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY264  obtain ⟨z, hz, zShape⟩ := quotient.representative with hZ265  rw [xShape, yShape, zShape]266  have sumYZ := quotientBinary.classes at A, r, add, y, z with *267  have sumXY := quotientBinary.classes at A, r, add, x, y with *268  have prodXY := quotientBinary.classes at A, r, mul, x, y with *269  have prodXZ := quotientBinary.classes at A, r, mul, x, z with *270  have prodYZ := quotientBinary.classes at A, r, mul, y, z with *271  have leftL := quotientBinary.classes at A, r, mul, x, call2(add, y, z) with *272  have rightL := quotientBinary.classes at A, r, add, call2(mul, x, y), call2(mul, x, z) with *273  have leftR := quotientBinary.classes at A, r, mul, call2(add, x, y), z with *274  have rightR := quotientBinary.classes at A, r, add, call2(mul, x, z), call2(mul, y, z) with *275  have ordinary := law with x, hx, y, hy, z, hz276  have leftLaw := ordinary.left277  have rightLaw := ordinary.right278  constructor279  . cc280  . cc281282283theorem quotient.comm_ring (A r add zero neg mul one : Set)284  requires ring : IsCommRing(A, add, zero, neg, mul, one)285  requires equivalence : Equivalence(A, r)286  requires addCompatible : CompatibleBinary(A, r, add)287  requires mulCompatible : CompatibleBinary(A, r, mul)288  requires negCompatible : CompatibleUnary(A, r, neg)289  shows IsCommRing((A ⧸ r), quotientBinary(A, r, add), ⟦zero⟧[A, r],290    quotientUnary(A, r, neg), quotientBinary(A, r, mul), ⟦one⟧[A, r])291proof292  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]293  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]294  have addAssoc : Associative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]295  have mulAssoc : Associative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]296  have addComm : Commutative(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]297  have mulComm : Commutative(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]298  have addUnit : Identity(A, add, zero) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]299  have mulUnit : Identity(A, mul, one) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]300  have inverse : Inverse(A, add, zero, neg) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]301  have distribute : Distributive(A, add, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]302  have qAdd := quotientBinary.magma at A, r, add with *303  have qMul := quotientBinary.magma at A, r, mul with *304  have qAddAssoc := quotientBinary.associative at A, r, add with *305  have qMulAssoc := quotientBinary.associative at A, r, mul with *306  have qAddComm := quotientBinary.commutative at A, r, add with *307  have qMulComm := quotientBinary.commutative at A, r, mul with *308  have qAddUnit := quotientBinary.identity at A, r, add, zero with *309  have qMulUnit := quotientBinary.identity at A, r, mul, one with *310  have qInverse := quotientUnary.inverse with *311  have qDistribute := quotientBinary.distributive with *312  simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]313