ForcingNames.lean`

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PartitionConsistency.SetForcingNames.Child line 13
Source documentation
The subname relation on literal set codes. The second component of an edge is a forcing condition; the first component is a name for a potential member.
```
def Child (τ σ : ZFSet.{u}) : Prop := ∃ p, ZFSet.pair τ p ∈ σ
```
theorem OAI.PartitionConsistency.SetForcingNames.child_wf line 15
def OAI.PartitionConsistency.SetForcingNames.Edges line 25
Source documentation
Edges of a set name, with no choice of a presentation of that set.
```
def Edges (σ : ZFSet.{u}) := {e : ZFSet.{u} × ZFSet.{u} // ZFSet.pair e.1 e.2 ∈ σ}
```
instance OAI.PartitionConsistency.SetForcingNames.(instance at line 27) line 27
def OAI.PartitionConsistency.SetForcingNames.IsName line 37
Source documentation
Well-formed set-forcing names. This is the usual hereditary recursive condition on sets of pairs, not a predicate on their interpreted values.
```
def IsName (P : Set ZFSet.{u}) : ZFSet.{u} → Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.isName_iff line 42
theorem OAI.PartitionConsistency.SetForcingNames.IsName.intro line 48
theorem OAI.PartitionConsistency.SetForcingNames.IsName.edges line 58
theorem OAI.PartitionConsistency.SetForcingNames.IsName.child line 64
theorem OAI.PartitionConsistency.SetForcingNames.IsName.condition line 68
theorem OAI.PartitionConsistency.SetForcingNames.isName_empty line 72
def OAI.PartitionConsistency.SetForcingNames.evaluate line 77
Source documentation
Interpretation of actual set-name codes. At no point is the forcing order or a maximum principle used in this recursion.
```
noncomputable def evaluate (G : Set ZFSet.{u}) : ZFSet.{u} → ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_eq line 81
theorem OAI.PartitionConsistency.SetForcingNames.mem_evaluate_iff line 86
def OAI.PartitionConsistency.SetForcingNames.mapConditions line 96
Source documentation
Recursive transport of names by a map on condition codes.
```
noncomputable def mapConditions (f : ZFSet.{u} → ZFSet.{u}) : ZFSet.{u} → ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_eq line 100
theorem OAI.PartitionConsistency.SetForcingNames.mem_mapConditions_iff line 106
theorem OAI.PartitionConsistency.SetForcingNames.edge_mapConditions_iff line 116
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_empty line 121
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_empty line 125
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_id line 130
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_comp line 143
theorem OAI.PartitionConsistency.SetForcingNames.IsName.mapConditions line 158
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_mapConditions line 169
Source documentation
Covariance holds with the filter transformed as well; this is not a claim that moving a name gives an automorphism of one fixed transitive extension.
```
theorem evaluate_mapConditions (f : ZFSet.{u} → ZFSet.{u}) (G : Set ZFSet.{u})
    (σ : ZFSet.{u}) : evaluate G (mapConditions f σ) = evaluate (f ⁻¹' G) σ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.evaluate, OAI.PartitionConsistency.SetForcingNames.mapConditions
def OAI.PartitionConsistency.SetForcingNames.checkName line 186
Source documentation
The canonical name for a ground set, using the condition t. In applications t is the largest condition.
```
noncomputable def checkName (t : ZFSet.{u}) : ZFSet.{u} → ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.checkName_eq line 189
theorem OAI.PartitionConsistency.SetForcingNames.mem_checkName_iff line 194
theorem OAI.PartitionConsistency.SetForcingNames.edge_checkName_iff line 199
theorem OAI.PartitionConsistency.SetForcingNames.checkName_isName line 203
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_checkName line 211
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_checkName line 225
def OAI.PartitionConsistency.SetForcingNames.pairName line 240
Source documentation
A literal pairing name.
```
def pairName (t σ τ : ZFSet.{u}) : ZFSet.{u} := {ZFSet.pair σ t, ZFSet.pair τ t}
```
theorem OAI.PartitionConsistency.SetForcingNames.pairName_isName line 242
theorem OAI.PartitionConsistency.SetForcingNames.edge_pairName_iff line 250
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_pairName line 254
theorem OAI.PartitionConsistency.SetForcingNames.mapConditions_pairName line 267
def OAI.PartitionConsistency.SetForcingNames.UnionEdges line 283
Source documentation
A small type indexing the three conditions used by the union-name construction: the two existing edge conditions and their common strengthening.
```
def UnionEdges (P : ZFSet.{u}) (R : ZFSet.{u} → ZFSet.{u} → Prop) (σ : ZFSet.{u}) :=
…
```
instance OAI.PartitionConsistency.SetForcingNames.(instance at line 287) line 287
def OAI.PartitionConsistency.SetForcingNames.unionName line 294
Source documentation
The union name for an arbitrary set forcing, not necessarily one with binary meets. Every common strengthening is included.
```
noncomputable def unionName (P : ZFSet.{u}) (R : ZFSet.{u} → ZFSet.{u} → Prop)
    (σ : ZFSet.{u}) : ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.mem_unionName_iff line 298
theorem OAI.PartitionConsistency.SetForcingNames.edge_unionName_iff line 309
theorem OAI.PartitionConsistency.SetForcingNames.unionName_isName line 319
theorem OAI.PartitionConsistency.SetForcingNames.evaluate_unionName line 328
Source documentation
Interpretation of the union constructor needs precisely upward closure and directedness of the filter. No continuity or closure of the poset is assumed.
```
theorem evaluate_unionName {P : ZFSet.{u}} {R : ZFSet.{u} → ZFSet.{u} → Prop}
    {G : Set ZFSet.{u}} (hGP : G ⊆ P)
    (hup : ∀ p ∈ P, ∀ q ∈ G, R q p → p ∈ G)
    (hdir : ∀ p ∈ G, ∀ r ∈ G, ∃ q ∈ G, R q p ∧ R q r)
    {σ : ZFSet.{u}} (hσ : IsName P σ) :
    evaluate G (unionName P R σ) = ZFSet.sUnion (evaluate G σ) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.IsName, OAI.PartitionConsistency.SetForcingNames.evaluate, OAI.PartitionConsistency.SetForcingNames.unionName
structure OAI.PartitionConsistency.SetForcingNames.ConditionAction line 354
Source documentation
The condition part of a symmetric system. A homomorphism into permutations of the actual set of conditions is enough to lift the action to set names. Preservation of the forcing order is used separately for the union constructor.
```
structure ConditionAction (Γ : Type v) [Group Γ] where
…
```
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode line 362
Source documentation
Extend a permutation of the conditions by the identity on all other codes.
```
noncomputable def actCode (g : Γ) (p : ZFSet.{u}) : ZFSet.{u} := by
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_of_mem line 366
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_of_not_mem line 371
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_mem line 376
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_one line 381
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_mul line 387
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_inv_actCode line 395
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_actCode_inv line 399
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.actCode_injective line 403
structure OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name line 408
Source documentation
Literal names for this condition set. Equality is equality of the underlying ZF sets, not equality of tree presentations.
```
structure Name where
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.ext line 415
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.act line 421
instance OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.(instance at line 425) line 425
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_val line 441
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.evaluate_smul line 445
Source documentation
The syntax action and evaluation transform together.
```
theorem evaluate_smul (g : Γ) (G : Set ZFSet.{u}) (σ : S.Name) :
    evaluate G (g • σ).val = evaluate (S.actCode g ⁻¹' G) σ.val :=
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.evaluate
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.child line 451
Source documentation
An edge recovers a name, with hereditary well-formedness proved from its parent rather than imposed as an additional hypothesis.
```
def child (σ : S.Name) {τ p : ZFSet.{u}} (he : ZFSet.pair τ p ∈ σ.val) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.child_val line 454
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.child_wellFounded line 457
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.check line 461
Source documentation
Canonical names in the actual condition system.
```
noncomputable def check {t : ZFSet.{u}} (ht : t ∈ S.conditions) (x : ZFSet.{u}) : S.Name :=
…
```
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.pair line 465
Source documentation
Pairing of names in the actual condition system.
```
def pair {t : ZFSet.{u}} (ht : t ∈ S.conditions) (σ τ : S.Name) : S.Name :=
…
```
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.union line 469
Source documentation
Union of names for the chosen forcing order.
```
noncomputable def union (R : ZFSet.{u} → ZFSet.{u} → Prop) (σ : S.Name) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_check line 472
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_pair line 479
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.mapConditions_unionName line 496
Source documentation
If condition permutations preserve the order, they commute exactly with the set-valued union-name constructor.
```
theorem mapConditions_unionName (R : ZFSet.{u} → ZFSet.{u} → Prop)
    (hR : ∀ g p q, R (S.actCode g p) (S.actCode g q) ↔ R p q)
    (g : Γ) (σ : ZFSet.{u}) :
    mapConditions (S.actCode g) (unionName S.conditions R σ) =
      unionName S.conditions R (mapConditions (S.actCode g) σ) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.mapConditions, OAI.PartitionConsistency.SetForcingNames.unionName
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_union line 528
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.Symmetric line 536
Source documentation
A name is symmetric when its literal set-name stabilizer belongs to the specified subgroup filter. This does not mention its interpretation.
```
def Symmetric (F : Set (Subgroup Γ)) (σ : S.Name) : Prop :=
…
```
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS line 541
Source documentation
Hereditary symmetry follows the subname relation, not membership of the interpreted sets.
```
def HS (F : Set (Subgroup Γ)) : S.Name → Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.hs_iff line 545
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS.symmetric line 550
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS.subname line 553
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS.child line 556
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS.smul line 562
Source documentation
Normality of the subgroup filter is exactly what is needed to transport hereditarily symmetric names.
```
theorem HS.smul {F : Set (Subgroup Γ)} (hF : SupportFilter.IsNormalFilter F) (g : Γ)
    {σ : S.Name} (hσ : HS F σ) : HS F (g • σ) := by
…
```
Mentions: OAI.PartitionConsistency.SupportFilter.IsNormalFilter, OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.HS
def OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.empty line 578
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.smul_empty line 580
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.empty_HS line 584
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.check_HS line 596
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.pair_HS line 613
theorem OAI.PartitionConsistency.SetForcingNames.ConditionAction.Name.union_HS line 628