Atoms #

In this file, we define atoms: the elements of the base type of our model. They are not atoms in the ZFU sense (for example), they are simply the elements of the model which are in type ⊥.

This base type does not appear in the final construction, it is just used as the foundation on which the subsequent layers can be built.

source

structure ConNF.Atom [ConNF.Params] :

Type u

The base type of the construction, denoted by τ₋₁ in various papers. An atom consists of a litter together with an index in κ. This gives a partition of atoms into litters: we say that two atoms are in the same litter if their first projections are equal. These equivalence classes will be called litter sets.

These are not 'atoms' in the ZFU, TTTU or NFU sense; they are simply the elements of the model which are in type τ₋₁.

litter : ConNF.Litter
index : ConNF.κ

Instances For

source

instance ConNF.instSuperLAtomLitter [ConNF.Params] :

ConNF.SuperL ConNF.Atom ConNF.Litter

If a is an atom, aᴸ is its first projection; that is, the litter associated to it.

Equations

ConNF.instSuperLAtomLitter = { superL := ConNF.Atom.litter }

source

instance ConNF.instSuperALitterSetAtom [ConNF.Params] :

ConNF.SuperA ConNF.Litter (Set ConNF.Atom)

If L is a litter, Lᴬ is the set of atoms associated to that litter. This is sometimes called the litter set of L.

Equations

ConNF.instSuperALitterSetAtom = { superA := fun (L : ConNF.Litter) => {a : ConNF.Atom | aᴸ = L} }

source

@[simp]

theorem ConNF.mem_litter_atoms_iff [ConNF.Params] (a : ConNF.Atom) (L : ConNF.Litter) :

a ∈ Lᴬ ↔ aᴸ = L

The definition of membership in a litter set.

source

theorem ConNF.Atom.ext [ConNF.Params] {a₁ a₂ : ConNF.Atom} (h : a₁ᴸ = a₂ᴸ) (h' : a₁.index = a₂.index) :

a₁ = a₂

source

def ConNF.atomEquiv [ConNF.Params] :

ConNF.Atom ≃ ConNF.Litter × ConNF.κ

Strips away the name of the type of atoms, converting it into a combination of types well-known to mathlib.

Equations

ConNF.atomEquiv = { toFun := fun (a : ConNF.Atom) => (aᴸ, a.index), invFun := fun (a : ConNF.Litter × ConNF.κ) => { litter := a.1, index := a.2 }, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem ConNF.card_atom [ConNF.Params] :

Cardinal.mk ConNF.Atom = Cardinal.mk ConNF.μ

The cardinality of Atom is the cardinality of μ. We will prove that all types constructed in our model have cardinality equal to that of μ.

source

def ConNF.litterSetEquiv [ConNF.Params] (L : ConNF.Litter) :

↑Lᴬ ≃ ConNF.κ

Each litter set is equivalent as a type to κ.

Equations

ConNF.litterSetEquiv L = { toFun := fun (a : ↑Lᴬ) => (↑a).index, invFun := fun (i : ConNF.κ) => ⟨{ litter := L, index := i }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }