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.

Main declarations #

ConNF.Atom: The type of atoms.

source

structure ConNF.Atom [ConNF.Params] :

Type u

The base type of the construction, denoted by τ₋₁ in various papers. Instead of declaring it as an arbitrary type of cardinality μ and partitioning it into suitable sets of litters afterwards, we define it as Litter × κ, which has the correct cardinality and comes with a natural partition.

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

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.

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

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 μ.

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 := ⋯ }