LocalQuotients.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Descent

theorem OAI.PartitionConsistency.ProductForcing.active_equal_independent line 18
Source documentation
Independently placed active copies are equal, for arbitrary-rank names. A shared third copy transports the given equality into a common extension of each potential counterexample, using the proved three-copy placement.
```
theorem active_equal_independent [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hinter : s₀.range ∩ s₁.range = p.range)
    (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (σ₀ σ₁ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.permute_le_root line 58
Source documentation
Root-preserving translates of a diagram still extend its root.
```
theorem permute_le_root (p s : Diagram M I) (hs : s ≤ p)
    (α : Equiv.Perm I) (hα : ∀ j ∈ p.range, α j = j) : s.permute α ≤ p := by
…
```
theorem OAI.PartitionConsistency.ProductForcing.active_equal line 67
Source documentation
Coherence for arbitrary overlaps. A third independent active copy can be placed compatibly below every proposed common extension; the independent comparison then identifies both given copies with that third one.
```
theorem active_equal [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hs₀ : s₀ ≤ p)
    (hinter : s₀.range ∩ s₁.range = p.range) (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (σ₀ σ₁ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.supported_mono line 120
Source documentation
Literal diagram support is inherited by stronger diagrams.
```
theorem supported_mono {p s : Diagram M I} (hsp : s ≤ p)
    (σ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system

theorem OAI.PartitionConsistency.ProductForcing.support_descent line 132

Source documentation

The unrestricted-rank support intersection lemma, in direct product forcing form. Both root equalities hold under the respective restrictions of the original Cohen witness, not under an extra compatibility hypothesis.

theorem support_descent [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hs₀ : s₀ ≤ p) (hs₁ : s₁ ≤ p)
    (hinter : s₀.range ∩ s₁.range = p.range) (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (σ₀ σ₁ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

Mentions: OAI.PartitionConsistency.ProductForcing.system

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separate_fixed line 218
Source documentation
Separation retains the literal common support of the bounding name and all of its parameters.
```
theorem separate_fixed {n} (σ : S.Name) (v : Fin n → S.Name)
    (φ : Formula (n+1)) (g : Γ) (hσ : g • σ = σ) (hv : ∀ i, g • v i = v i) :
    g • S.separate σ v φ = S.separate σ v φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.normalize_fixed line 226
Source documentation
Normalizing a subset name does not enlarge its support.
```
theorem normalize_fixed (σ ν : S.Name) (g : Γ)
    (hσ : g • σ = σ) (hν : g • ν = ν) :
    g • S.normalize σ ν = S.normalize σ ν := by
…
```
theorem OAI.PartitionConsistency.ProductForcing.labelSet_subsetBound line 247
Source documentation
The normalization bound is the actual set of all pairs of individual label names with condition codes; there is no bound on the ranks of the original subsets being represented.
```
theorem labelSet_subsetBound :
    (system (M := M) (I := I) (κ := κ) hμ).subsetBound (labelSet hμ c) =
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet
theorem OAI.PartitionConsistency.ProductForcing.normalized_subset_labelSet line 271
Source documentation
Every normalized candidate is forced to be a subset of the label set, not just those candidates which happen to be classes for a particular E.
```
theorem normalized_subset_labelSet
    (ν : (system (M := M) (I := I) (κ := κ) hμ).PowerCandidate (labelSet hμ c))
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet
def OAI.PartitionConsistency.ProductForcing.LocalName line 289
Source documentation
The ground collection X(r): all normalized subset names supported literally by the diagram range. It is a set, rather than an unrestricted class of HS names.
```
def LocalName (r : Diagram M I) :=
…
```
instance OAI.PartitionConsistency.ProductForcing.(instance at line 293) line 293
def OAI.PartitionConsistency.ProductForcing.LocalName.name line 300
theorem OAI.PartitionConsistency.ProductForcing.LocalName.fixed line 303
theorem OAI.PartitionConsistency.ProductForcing.LocalName.ext line 306
def OAI.PartitionConsistency.ProductForcing.LocalName.restrict line 309
theorem OAI.PartitionConsistency.ProductForcing.LocalName.restrict_name line 313
theorem OAI.PartitionConsistency.ProductForcing.LocalName.restrict_restrict line 316
theorem OAI.PartitionConsistency.ProductForcing.LocalName.restrict_injective line 319
def OAI.PartitionConsistency.ProductForcing.localNormalize line 327
Source documentation
Canonical normalization into X(r), for any supported name at any rank.
```
def localNormalize (r : Diagram M I)
    (ν : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.localNormalize_eq line 333
theorem OAI.PartitionConsistency.ProductForcing.localName_of_raw line 342
Source documentation
Every literally supported raw subset of the normalization bound is HS. Thus X(r) omits no supported normalized name by using the HS-name type.
```
theorem localName_of_raw (hcard : Cardinal.mk M ≤ μ) (r : Diagram M I)
    (ν : ZFSet.{u})
    (hb : ν ⊆ (system (M := M) (I := I) (κ := κ) hμ).subsetBound (labelSet hμ c))
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.labelSet

theorem OAI.PartitionConsistency.ProductForcing.localName_descent line 374

Source documentation

Support descent followed by normalization supplies a member of the ground set X(p), with the equalities at the two original supporting roots. No statement that the descended name is a class is postulated here.

theorem localName_descent [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hs₀ : s₀ ≤ p) (hs₁ : s₁ ≤ p)
    (hinter : s₀.range ∩ s₁.range = p.range) (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (σ₀ : LocalName hμ c s₀) (σ₁ : LocalName hμ c s₁)
    (d : CohenForcing.Condition I κ)
    (heq : (system hμ).atomic.EqF ((d,v) : Poset M I κ) σ₀.name σ₁.name) :
    ∃ σ : LocalName hμ c p,
      (system hμ).atomic.EqF ((d.restrict s₀.range,s₀) : Poset M I κ) σ.name σ₀.name ∧
      (system hμ).atomic.EqF ((d.restrict s₁.range,s₁) : Poset M I κ) σ.name σ₁.name := by
…

Mentions: OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset

def OAI.PartitionConsistency.ForcingQuotient.GenericFilter.move line 409
Source documentation
Transport of a filter along an order automorphism. It transports the filter, not the interpretation of all names in a single fixed extension.
```
def GenericFilter.move (F : GenericFilter P) (e : P ≃o P) : GenericFilter P where
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter
theorem OAI.PartitionConsistency.ForcingQuotient.GenericFilter.mem_move line 430
def OAI.PartitionConsistency.ProductForcing.localAtomic line 445
Source documentation
Atomic forcing at a fixed ground diagram, retaining the Cohen coordinate as the forcing parameter. Its laws follow from actual product forcing.
```
def localAtomic (r : Diagram M I) :
    AtomicData (CohenForcing.Condition I κ) (system (M := M) (I := I) (κ := κ) hμ).Name where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.localSetoid line 457
Source documentation
The local equality relation is witnessed by a Cohen condition in F.
```
def localSetoid (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I) :
    Setoid (LocalName hμ c r) where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName
def OAI.PartitionConsistency.ProductForcing.LocalQuotient line 466
Source documentation
All local normalized subsets modulo local forced equality. The local E-class sets used subsequently are subcollections of this actual quotient.
```
def LocalQuotient (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
instance OAI.PartitionConsistency.ProductForcing.(instance at line 469) line 469
def OAI.PartitionConsistency.ProductForcing.LocalQuotient.ofName line 477
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.ofName_eq line 480
def OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict line 485
Source documentation
Retaining the same representative gives the restriction/inclusion map.
```
def restrict {r s : Diagram M I} (hsr : s ≤ r) :
    LocalQuotient (c := c) hμ F r → LocalQuotient (c := c) hμ F s :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalQuotient
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict_ofName line 495
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict_refl line 498
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict_restrict line 503
theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict_injective line 511
Source documentation
Local decision prevents a stronger diagram from identifying distinct local classes. No genericity hypothesis on F is needed for this direction.
```
theorem restrict_injective [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    {r s : Diagram M I} (hsr : s ≤ r) :
    Function.Injective (restrict (c := c) (hμ := hμ) F hsr) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalQuotient.restrict

theorem OAI.PartitionConsistency.ProductForcing.LocalQuotient.intersection line 536

Source documentation

The intersection property of local symbolic subsets. This is the quotient-level consequence of the proved arbitrary-rank support descent.

theorem intersection [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hs₀ : s₀ ≤ p) (hs₁ : s₁ ≤ p)
    (hinter : s₀.range ∩ s₁.range = p.range) (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (x₀ : LocalQuotient (c := c) hμ F s₀) (x₁ : LocalQuotient (c := c) hμ F s₁)
…

Mentions: OAI.PartitionConsistency.ProductForcing.LocalQuotient

def OAI.PartitionConsistency.ProductForcing.LocalName.transport line 560
Source documentation
Literal transport carries the entire local-name collection to the moved diagram, including normalization and the full supporting fixer.
```
def LocalName.transport {r : Diagram M I} (π : Equiv.Perm I) (σ : LocalName hμ c r) :
    LocalName hμ c (r.permute π) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.LocalName.transport_name line 571
def OAI.PartitionConsistency.ProductForcing.LocalQuotient.transport line 576
Source documentation
Transport of local symbolic names is between F and πF. This is not an action on some fixed evaluated universe.
```
def LocalQuotient.transport (F : GenericFilter (CohenForcing.Condition I κ))
    (π : Equiv.Perm I) {r : Diagram M I} :
    LocalQuotient (c := c) hμ F r →
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalQuotient