Structural Transport

SE.Individuation.Structural.Transport

A bijection between eligible domains that preserves and reflects whole co-membership transports whole supports and their equality and disjointness relations. For the connectivity instance, a bijection that preserves and reflects bonds is sufficient.

Presentation-level transport additionally needs a presentation map that preserves and reflects admissibility and carries supports to their corresponding images.

These results establish invariance of the construction under the stated transport. They do not establish strict identity across settings.

structure SE.Individuation.Structural.EligibleIso {A₁ P₁ : Type u} {A₂ P₂ : Type v} (s₁ : Setting A₁ P₁) (s₂ : Setting A₂ P₂) : Type (max u v)

A bijection between eligible domains preserving and reflecting whole co-membership.

• toFun : { a : A₁ // a ∈ s₁.eligible } → { b : A₂ // b ∈ s₂.eligible }

  The forward map between eligible elements.

• invFun : { b : A₂ // b ∈ s₂.eligible } → { a : A₁ // a ∈ s₁.eligible }

  The inverse map between eligible elements.

• left_inv (x : { a : A₁ // a ∈ s₁.eligible }) : self.invFun (self.toFun x) = x

  invFun is a left inverse of toFun.

• right_inv (y : { b : A₂ // b ∈ s₂.eligible }) : self.toFun (self.invFun y) = y

  toFun is a right inverse of invFun.

• preserves (x y : { a : A₁ // a ∈ s₁.eligible }) : s₁.E x y → s₂.E (self.toFun x) (self.toFun y)

  toFun preserves the setting's structure.

• reflects (x y : { a : A₁ // a ∈ s₁.eligible }) : s₂.E (self.toFun x) (self.toFun y) → s₁.E x y

  toFun reflects the setting's structure: related images come from related elements.

def SE.Individuation.Structural.EligibleIso.image {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) (W : MathlibMini.Set A₁) : MathlibMini.Set A₂

The image of a set of atoms: images of its eligible atoms.

Equations

• f.image W b = ∃ (x : { a : A₁ // a ∈ s₁.eligible }), x.val ∈ W ∧ (f.toFun x).val = b

theorem SE.Individuation.Structural.EligibleIso.mem_image_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) (x : { a : A₁ // a ∈ s₁.eligible }) (W : MathlibMini.Set A₁) : (f.toFun x).val ∈ f.image W ↔ x.val ∈ W

An element lies in the image exactly when it comes from an eligible element.

theorem SE.Individuation.Structural.EligibleIso.coMember_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) (a b : A₁) (ha : a ∈ s₁.eligible) (hb : b ∈ s₁.eligible) : s₁.CoMember a b ↔ s₂.CoMember (f.toFun ⟨a, ha⟩).val (f.toFun ⟨b, hb⟩).val

Co-membership of eligible atoms is preserved and reflected.

theorem SE.Individuation.Structural.EligibleIso.wholeConditions_image_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) {W : MathlibMini.Set A₁} (hW : W ⊆ s₁.eligible) : s₁.WholeConditions W ↔ s₂.WholeConditions (f.image W)

The whole conditions are invariant under structural transport of sets inside the eligible domain.

theorem SE.Individuation.Structural.EligibleIso.image_eq_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) {W₁ W₂ : MathlibMini.Set A₁} (h₁ : W₁ ⊆ s₁.eligible) (h₂ : W₂ ⊆ s₁.eligible) : f.image W₁ = f.image W₂ ↔ W₁ = W₂

Transport preserves and reflects equality of sets inside the eligible domain.

theorem SE.Individuation.Structural.EligibleIso.image_disjoint_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) {W₁ W₂ : MathlibMini.Set A₁} (h₁ : W₁ ⊆ s₁.eligible) : (∀ (b : A₂), b ∈ f.image W₁ → ¬b ∈ f.image W₂) ↔ ∀ (a : A₁), a ∈ W₁ → ¬a ∈ W₂

Transport preserves and reflects disjointness of sets, given the first lies in the eligible domain.

def SE.Individuation.Structural.EligibleIso.ofBondCorrespondence {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} {bond₁ : { a : A₁ // a ∈ s₁.eligible } → { a : A₁ // a ∈ s₁.eligible } → Prop} {bond₂ : { b : A₂ // b ∈ s₂.eligible } → { b : A₂ // b ∈ s₂.eligible } → Prop} (hs₁ : s₁.BondGenerated bond₁) (hs₂ : s₂.BondGenerated bond₂) (toFun : { a : A₁ // a ∈ s₁.eligible } → { b : A₂ // b ∈ s₂.eligible }) (invFun : { b : A₂ // b ∈ s₂.eligible } → { a : A₁ // a ∈ s₁.eligible }) (left_inv : ∀ (x : { a : A₁ // a ∈ s₁.eligible }), invFun (toFun x) = x) (right_inv : ∀ (y : { b : A₂ // b ∈ s₂.eligible }), toFun (invFun y) = y) (bond_iff : ∀ (x y : { a : A₁ // a ∈ s₁.eligible }), bond₁ x y ↔ bond₂ (toFun x) (toFun y)) : EligibleIso s₁ s₂

For the connectivity instance, a bijection of eligible atoms that preserves and reflects bonds gives a structural transport.

Equations

• One or more equations did not get rendered due to their size.

structure SE.Individuation.Structural.PresentationTransport {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} (f : EligibleIso s₁ s₂) : Type (max u v)

A presentation map that preserves and reflects admissibility and carries supports to images.

• toFun : P₁ → P₂

  The map on presentations.

• admissible_iff (p : P₁) : s₂.admissible (self.toFun p) ↔ s₁.admissible p

  A presentation is admissible exactly when its image under toFun is admissible.

• support_eq (p : P₁) : s₁.admissible p → s₂.support (self.toFun p) = f.image (s₁.support p)

  toFun carries a presentation's support to the corresponding support.

theorem SE.Individuation.Structural.PresentationTransport.succeeds_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} {f : EligibleIso s₁ s₂} (g : PresentationTransport f) (p : P₁) : s₁.Succeeds p ↔ s₂.Succeeds (g.toFun p)

Success is invariant under presentation transport.

theorem SE.Individuation.Structural.PresentationTransport.sameUnit_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} {f : EligibleIso s₁ s₂} (g : PresentationTransport f) (p q : P₁) : s₁.SameUnit p q ↔ s₂.SameUnit (g.toFun p) (g.toFun q)

Same-unit identity is invariant under presentation transport.

theorem SE.Individuation.Structural.PresentationTransport.distinctUnits_iff {A₁ P₁ : Type u} {A₂ P₂ : Type v} {s₁ : Setting A₁ P₁} {s₂ : Setting A₂ P₂} {f : EligibleIso s₁ s₂} (g : PresentationTransport f) (p q : P₁) : s₁.DistinctUnits p q ↔ s₂.DistinctUnits (g.toFun p) (g.toFun q)

Distinct-unit judgments are invariant under presentation transport.