Grace/Cumulus/Set/Zorn.g17

Open in Workbench Download source

Imports

Cardinal.Hartogs · ChoiceFunctions

Declarations

Source

1-- Zorn's lemma from the axiom of choice and Hartogs' theorem.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 Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module Grace.Cumulus.Set.Zorn9import Cardinal.Hartogs10import ChoiceFunctions1112predicate NoMaximal (A r : Set) := ∀ x ∈ A, ¬Maximal(A, r, x)13def strictUpperBounds (A r C : Set) : Set :=14  {u ∈ A | ∀ x ∈ C, relates(r, x, u) ∧ x ≠ u}1516theorem strictUpperBounds.subset (A r C : Set)17  shows strictUpperBounds(A, r, C) ⊆ A18proof19  simp2021theorem NoMaximal.extension (A r u : Set)22  requires noMaximal : NoMaximal(A, r)23  requires hu : u ∈ A24  shows ∃ v ∈ A, relates(r, u, v) ∧ v ≠ u25proof26  by_contra noExtension27  apply noMaximal with u, hu28  constructor29  . exact hu30  . intros v hv edge31    by_contra distinct32    apply noExtension33    refine ⟨v, hv, edge, distinct⟩3435theorem strictUpperBounds.nonempty (A r C : Set)36  requires zorn : ZornCondition(A, r)37  requires noMaximal : NoMaximal(A, r)38  requires chain : Chain(A, r, C)39  shows Nonempty(strictUpperBounds(A, r, C))40proof41  have order := ZornCondition.order with zorn42  have transitive := IsPartialOrder.transitive with order43  have antisymmetric := IsPartialOrder.antisymmetric with order44  obtain ⟨u, upper⟩ := ZornCondition.upper_bound with zorn, chain45  rcases upper with ⟨hu, subset, bounds⟩46  obtain ⟨v, hv, uv, distinct⟩ := NoMaximal.extension with noMaximal, hu47  witness v48  apply strictUpperBounds.membership.backward49  constructor50  . exact hv51  . intros x hx52    have hxA := subset with x, hx53    have xu := bounds with x, hx54    have xv := transitive with x, hxA, u, hu, v, hv, xu, uv55    constructor56    . exact xv57    . intro equal58      rw equal at xu59      have same := antisymmetric with v, hv, u, hu, xu, uv60      exact distinct with same6162-- At stage x choose a strict upper bound of all earlier values. The term is63-- total; its useful laws below require a choice function and no maximal point.64theorem zornStep.well_founded (A r H c : Set)65  shows wellFoundedOn(membershipOn(H), H)66proof67  simp [membershipOn.wellFounded]6869noncomputable well-founded def zornStep (A r H c x : Set) : Set70  over H ordered by membershipOn(H)71  certified by zornStep.well_founded72  | x using history => c[strictUpperBounds(A, r, Relation.range(history))]7374def zornEarlier (A r H c x : Set) : Set := Relation.range(zornStep.history(A, r, H, c, x))7576theorem zornEarlier.membership (z A r H c x : Set)77  shows z ∈ zornEarlier(A, r, H, c, x) ↔78    ∃ y ∈ H, relates(membershipOn(H), y, x) ∧ z = zornStep(A, r, H, c, y)79proof80  constructor81  . intro member82    unfold zornEarlier at member83    obtain ⟨bounded, source, pair⟩ := Relation.range.membership.forward with member84    obtain ⟨y, hy, earlier, equal⟩ := zornStep.history.membership.forward with pair85    obtain ⟨sameSource, sameValue⟩ := orderedPair.injective with equal86    refine ⟨y, hy, earlier, sameValue⟩87  . intro represented88    obtain ⟨y2, hy2, earlier2, value2⟩ := represented89    have pair2 : (y2, zornStep(A, r, H, c, y2)) ∈ zornStep.history(A, r, H, c, x)90      exact zornStep.history.membership.backward with ⟨y2, hy2, earlier2, rfl⟩91    have rangeMember := Relation.range.contains with pair292    unfold zornEarlier93    rwa value29495theorem zornStep.selects (A r H c x : Set)96  requires hx : x ∈ H97  shows zornStep(A, r, H, c, x) = c[strictUpperBounds(A, r, zornEarlier(A, r, H, c, x))]98proof99  have equation := zornStep.equation.direct at A, r, H, c, x with hx100  simpa [zornEarlier] using equation101102predicate ZornPosition (A r H c x : Set) :=103  zornStep(A, r, H, c, x) ∈ A ∧104  (∀ y ∈ H, relates(membershipOn(H), y, x) →105    relates(r, zornStep(A, r, H, c, y), zornStep(A, r, H, c, x)) ∧106    zornStep(A, r, H, c, y) ≠ zornStep(A, r, H, c, x))107108theorem zornStep.position (A r H c : Set)109  requires ordinal : H ∈ Ordinal110  requires zorn : ZornCondition(A, r)111  requires noMaximal : NoMaximal(A, r)112  requires choice : SubsetChoice(c, A)113  shows ∀ x ∈ H, ZornPosition(A, r, H, c, x)114proof115  have order := ZornCondition.order with zorn116  have reflexive := IsPartialOrder.reflexive with order117  induction x over H ordered by membershipOn(H) certified by membershipOn.wellFounded at H118  intros x hx ih119  have chain : Chain(A, r, zornEarlier(A, r, H, c, x))120    constructor121      intros u member122      obtain ⟨y, hy, earlier, value⟩ := zornEarlier.membership.forward with member123      obtain ⟨closed, increasing⟩ := ih with y, ⟨hy, earlier⟩124      rwa value125    . intros u hu v hv126      obtain ⟨a, ha, ax, uValue⟩ := zornEarlier.membership.forward with hu127      obtain ⟨b, hb, bx, vValue⟩ := zornEarlier.membership.forward with hv128      obtain ⟨aClosed, aIncreasing⟩ := ih with a, ⟨ha, ax⟩129      obtain ⟨bClosed, bIncreasing⟩ := ih with b, ⟨hb, bx⟩130      have aOrdinal := Ordinal.member with ordinal, ha131      have bOrdinal := Ordinal.member with ordinal, hb132      have alternatives := Ordinal.trichotomy with aOrdinal, b, bOrdinal133      unfold Comparable134      rw [uValue, vValue]135      cases alternatives with ab | rest136      . have earlierAB := membershipOn.relates.backward with ha, hb, ab137        obtain ⟨edgeAB, distinctAB⟩ := bIncreasing with a, ha, earlierAB138        left139        exact edgeAB140      . cases rest with equal | ba141        . rw equal142          left143          exact reflexive with zornStep(A, r, H, c, b), bClosed144        . have earlierBA := membershipOn.relates.backward with hb, ha, ba145          obtain ⟨edgeBA, distinctBA⟩ := aIncreasing with b, hb, earlierBA146          right147          exact edgeBA148  have inhabited := strictUpperBounds.nonempty with *149  have subset := strictUpperBounds.subset at A, r, zornEarlier(A, r, H, c, x)150  have selected := SubsetChoice.member with *151  have equation := zornStep.selects at A, r, H, c, x with hx152  have member : zornStep(A, r, H, c, x) ∈ strictUpperBounds(A, r, zornEarlier(A, r, H, c, x)) by rwa equation153  obtain ⟨closed, above⟩ := strictUpperBounds.membership.forward with member154  constructor155  . exact closed156  . intros y hy earlier157    have prior : zornStep(A, r, H, c, y) ∈ zornEarlier(A, r, H, c, x) := zornEarlier.membership.backward with ⟨y, hy, earlier, rfl⟩158    exact above with zornStep(A, r, H, c, y), prior159160defgraph zornSequence (A r H c : Set) (x ∈ H) : A := zornStep(A, r, H, c, x)161requires ordinal : H ∈ Ordinal162requires zorn : ZornCondition(A, r)163requires noMaximal : NoMaximal(A, r)164requires choice : SubsetChoice(c, A)165proof166  have position := zornStep.position with *167  obtain ⟨closed, increasing⟩ := position with x, assumption168  exact closed169170theorem zornSequence.injective (A r H c : Set)171  requires ordinal : H ∈ Ordinal172  requires zorn : ZornCondition(A, r)173  requires noMaximal : NoMaximal(A, r)174  requires choice : SubsetChoice(c, A)175  shows InjectiveBetween(zornSequence(A, r, H, c), H, A)176proof177  have function := zornSequence.function at A, r, H, c with *178  have positions := zornStep.position at A, r, H, c with *179  constructor180  . exact function181  . intros x hx y hy z hz mappedX mappedY182    have valueX := FunctionBetween.apply_value at zornSequence(A, r, H, c), H, A, x, z with *183    have valueY := FunctionBetween.apply_value at zornSequence(A, r, H, c), H, A, y, z with *184    have stepX := zornSequence.value at A, r, H, c, x with *185    have stepY := zornSequence.value at A, r, H, c, y with *186    have equalValues : zornStep(A, r, H, c, x) = zornStep(A, r, H, c, y) by cc187    have xOrdinal := Ordinal.member with ordinal, hx188    have yOrdinal := Ordinal.member with ordinal, hy189    have alternatives := Ordinal.trichotomy with xOrdinal, y, yOrdinal190    cases alternatives with xy | rest191    . have positionY := positions with y, hy192      rcases positionY with ⟨closedY, increasingY⟩193      have ruleXY := membershipOn.relates with hx, hy194      have earlierXY := ruleXY.backward with xy195      obtain ⟨edgeXY, distinctXY⟩ := increasingY with x, hx, earlierXY196      exfalso197      exact distinctXY with equalValues198    . cases rest with equal | yx199      . exact equal200      . have positionX := positions with x, hx201        rcases positionX with ⟨closedX, increasingX⟩202        have ruleYX := membershipOn.relates with hy, hx203        have earlierYX := ruleYX.backward with yx204        obtain ⟨edgeYX, distinctYX⟩ := increasingX with y, hy, earlierYX205        exfalso206        apply distinctYX207        symm208        exact equalValues209210theorem Zorn.theorem (A r : Set)211  requires zorn : ZornCondition(A, r)212  shows ∃ m, Maximal(A, r, m)213proof214  obtain ⟨c, choice⟩ := SubsetChoice.exists at A215  by_contra none216  have noMaximal : NoMaximal(A, r)217    intros x hx maximal218    apply none219    witness x220    exact maximal221  have ordinal := hartogsBound.ordinal at A222  have injection := zornSequence.injective with *223  exact hartogsBound.no_injection with injection224225-- A first application: every partial order has a maximal chain.226def chains (A r : Set) : Set := {C ∈ 𝒫(A) | Chain(A, r, C)}227228theorem chains.contains (C A r : Set)229  requires chain : Chain(A, r, C)230  shows C ∈ chains(A, r)231proof232  have subset := Chain.subset with chain233  unfold Subset at subset234  have bounded := set.powerset.backward with subset235  exact chains.membership.backward with ⟨bounded, chain⟩236237theorem chains.zorn (A r : Set)238  shows ZornCondition(chains(A, r), inclusionOrder(chains(A, r)))239proof240  constructor241  . exact inclusionOrder.partial at chains(A, r)242  . intros S chainS243    rcases chainS with ⟨subsetS, comparable⟩244    have family : ChainOfChains(A, r, S)245      constructor246      . intros C hC247        have member := subsetS with C, hC248        obtain ⟨bounded, chainC⟩ := chains.membership.forward with member249        exact chainC250      . intros C hC D hD251        have memberC := subsetS with C, hC252        have memberD := subsetS with D, hD253        have directions := comparable with C, hC, D, hD254        have forward := inclusionOrder.relates with memberC, memberD255        have backward := inclusionOrder.relates with memberD, memberC256        cases directions with cd | dc257        . left258          exact forward.forward with cd259        . right260          exact backward.forward with dc261    have unionChain := Chain.union with family262    have unionMember := chains.contains with unionChain263    witness ⋃(S)264    constructor265    . exact unionMember266    . constructor267        exact subsetS268      . intros C hC269        have memberC := subsetS with C, hC270        have rule := inclusionOrder.relates with memberC, unionMember271        apply rule.backward272        intros x hx273        exact set.union.backward with ⟨C, hC, hx⟩274275theorem Chain.exists_maximal (A r : Set)276  shows ∃ C, Chain(A, r, C) ∧ (∀ D, Chain(A, r, D) → C ⊆ D → D = C)277proof278  have condition := chains.zorn at A, r279  obtain ⟨C, maximal⟩ := Zorn.theorem with condition280  rcases maximal with ⟨memberC, greatest⟩281  obtain ⟨bounded, chainC⟩ := chains.membership.forward with memberC282  witness C283  constructor284  . exact chainC285  . intros D chainD subset286    have memberD := chains.contains with chainD287    have rule := inclusionOrder.relates with memberC, memberD288    have extension := rule.backward with subset289    exact greatest with D, memberD, extension290