OAI/CategoryTheory/Thomason/Gray/StrictAbelianization.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Identifying the strict globe with its positive chain realization

The canonical globe map is injective as well as surjective: the highest nonzero chain records the dimension and sign of its unique generator.

  1. abbrev OAI.Thomason.Construction.DirectedGlobeComplex.globeDimension line 25
  2. def OAI.Thomason.Construction.DirectedGlobeComplex.globeBasis line 28
  3. theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_top_table line 34
  4. theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_dimension_iff line 44
  5. theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_injective line 62

    Source documentation

    Distinct signed globe cells remain distinct after positive realization.

    theorem fromGlobe_injective (n : ℕ) : Function.Injective (fromGlobe n).toFun := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe

  6. def OAI.Thomason.Construction.DirectedGlobeComplex.globeIso line 93

    Source documentation

    The strict globe and its positive-table realization are isomorphic.

    def globeIso (n : ℕ) : StrictOmegaCategory.Globe.category n ≅ (complex n).realization :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.DirectedGlobeComplex.complex

  7. theorem OAI.Thomason.Construction.DirectedGlobeComplex.globeIso_hom line 97
  8. def OAI.Thomason.Construction.DirectedGlobeComplex.realizationHomEquiv line 101

    Source documentation

    On the free globes, taking strict realization is a full and faithful bijection of positive chain maps with actual strict functors.

    def realizationHomEquiv (n : ℕ) (K : DirectedComplex.{0}) :
    Hom (complex n) K ≃ ((complex n).realization ⟶ K.realization) where
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex

  9. structure OAI.Thomason.Construction.StrictOmegaCategory.Globe.Shapes line 134

    Source documentation

    The small category of strict globe parameters and all strict maps.

    structure Shapes where
…
  10. instance OAI.Thomason.Construction.StrictOmegaCategory.Globe.(instance at line 137) line 137
  11. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion line 145
  12. def OAI.Thomason.Construction.DirectedGlobeComplex.chainMap line 158

    Source documentation

    The unique positive map presenting an arbitrary strict globe map.

    def chainMap {m n : ℕ} (f : StrictOmegaCategory.Globe.category m ⟶
    StrictOmegaCategory.Globe.category n) : Hom (complex m) (complex n) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.DirectedGlobeComplex.complex

  13. theorem OAI.Thomason.Construction.DirectedGlobeComplex.chainMap_realization line 163
  14. def OAI.Thomason.Construction.DirectedGlobeComplex.chainFunctor line 168
  15. def OAI.Thomason.Construction.DirectedGlobeComplex.chainRealizationIso line 192

    Source documentation

    The comparison is natural for every strict map between globes.

    def chainRealizationIso : chainFunctor ⋙ realizationFunctor ≅
    StrictOmegaCategory.Globe.inclusion :=
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.chainFunctor, OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion

  16. def OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder line 202

    Source documentation

    The concrete signed right-cylinder functor on all strict globe maps.

    def rightGlobeCylinder : StrictOmegaCategory.Globe.Shapes ⥤ StrictOmegaCategory.{0} :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.Shapes

  17. def OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeEndpoint line 206

    Source documentation

    The two endpoint inclusions in the concrete globe cylinders.

    def rightGlobeEndpoint (a : Bool) : StrictOmegaCategory.Globe.inclusion ⟶
    rightGlobeCylinder where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion, OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder

  18. def OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeProjection line 238

    Source documentation

    The natural collapse returns the actual strict globe.

    def rightGlobeProjection : rightGlobeCylinder ⟶ StrictOmegaCategory.Globe.inclusion where
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeCylinder, OAI.Thomason.Construction.StrictOmegaCategory.Globe.inclusion

  19. theorem OAI.Thomason.Construction.DirectedGlobeComplex.rightGlobeEndpoint_projection line 266
  20. abbrev OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.CylinderIndex line 307
  21. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.zeroIndexEquiv line 309
  22. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.succIndexEquiv line 319
  23. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderCoordinates line 337

    Source documentation

    Coordinates are formed by the actual endpoint and mixed direct sums.

    noncomputable def cylinderCoordinates : (p : ℕ) →
    (rightCylinder K).group p ≃+ (B.CylinderIndex p →₀ ℤ)
  | 0 =>
    (AddEquiv.prodCongr (B.coordinates 0) (B.coordinates 0)).trans
      (Finsupp.sumFinsuppAddEquivProdFinsupp.symm.trans
        (Finsupp.domCongr B.zeroIndexEquiv.symm))
  | p+1 =>
    (AddEquiv.prodCongr (B.coordinates (p+1))
      (AddEquiv.prodCongr (B.coordinates (p+1)) (B.coordinates p))).trans
      ((AddEquiv.prodCongr (AddEquiv.refl _)
        Finsupp.sumFinsuppAddEquivProdFinsupp.symm).trans
        (Finsupp.sumFinsuppAddEquivProdFinsupp.symm.trans
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder

  24. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderCoefficient line 351
  25. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderCoordinates_apply line 358
  26. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinder_positive_iff line 367

    Source documentation

    These exact coordinates characterize the actual positive tensor cone.

    theorem cylinder_positive_iff (p : ℕ) (x : (rightCylinder K).group p) :
    x ∈ (rightCylinder K).positive p ↔ ∀ b, 0 ≤ B.cylinderCoordinates p x b := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder

  27. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinder_augmentation line 397

    Source documentation

    The ordinary tensor augmentation is the sum of all degree-zero coordinates, with neither endpoint omitted.

    theorem cylinder_augmentation (x : (rightCylinder K).group 0) :
    (rightCylinder K).augmentation x =
      (B.cylinderCoordinates 0 x).sum (fun _ z => z) := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder

  28. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderVector line 407

    Source documentation

    The basis vectors in the actual tensor coordinates.

    noncomputable def cylinderVector {p : ℕ} (b : B.CylinderIndex p) : (rightCylinder K).group p :=
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder

  29. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderVector_coordinates line 410
  30. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_dimension line 430
  31. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderAtom line 434
  32. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderAtom_dimension line 438
  33. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderAtom_above line 444
  34. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderAtom_top line 448
  35. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.SideHeight line 499

    Source documentation

    The stronger side-height information used when tensoring the basis. It is supplied by the already proved signed simplex boundary order.

    def SideHeight : Prop := ∀ p (b : B.Index p) q, q < p → ∀ (side : Bool) (c : B.Index q),
…
  36. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_side_height_le line 503
  37. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.prismSide_sourceEndpoint line 517
  38. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.prismSide_targetEndpoint line 523
  39. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.prism_endpoint_height line 530

    Source documentation

    The shifted rank of the endpoint selected by the prism has the exact sign of that prism side.

    theorem prism_endpoint_height (p : ℕ) (b : B.Index p) (side : Bool) :
    RightCylinderBasis.height B.height (.endpoint (RightCylinder.prismSide p side) b) =
      3 * B.height p b + if side then 1 else -1 := by
…

    Mentions: OAI.Thomason.Construction.RightCylinderBasis.height, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismSide

  40. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.endpointAtom_endpointCoefficient line 537
  41. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.endpointAtom_mixedCoefficient line 546
  42. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.mixedAtom_mixedCoefficient line 553
  43. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.mixedAtom_endpointCoefficient line 560
  44. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinderAtom_side_height line 577

    Source documentation

    Every strict lower face of an actual endpoint or prism atom has the required strict signed-height bound.

    theorem cylinderAtom_side_height (hs : B.SideHeight) {p : ℕ} (b : B.CylinderIndex p)
    (side : Bool) (q : ℕ) (hqp : q < p) (c : B.CylinderIndex q)
    (hc : B.cylinderCoefficient c ((B.cylinderAtom b).table side q) ≠ 0) :
    if side then RightCylinderBasis.height B.height b < RightCylinderBasis.height B.height c
    else RightCylinderBasis.height B.height c < RightCylinderBasis.height B.height b := by
…

    Mentions: OAI.Thomason.Construction.RightCylinderBasis.height

  45. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.cylinder_atoms_disjoint line 622

    Source documentation

    The concrete tensor atoms therefore have disjoint ordered boundaries.

    theorem cylinder_atoms_disjoint (hs : B.SideHeight) {p q r : ℕ}
    (b : B.CylinderIndex p) (c : B.CylinderIndex q) (hrp : r < p) (hrq : r < q)
    (hbc : RightCylinderBasis.height B.height b ≤ RightCylinderBasis.height B.height c)
    (e : B.CylinderIndex r) :
    B.cylinderCoordinates r ((B.cylinderAtom b).table false r) e = 0 ∨
      B.cylinderCoordinates r ((B.cylinderAtom c).table true r) e = 0 := by
…

    Mentions: OAI.Thomason.Construction.RightCylinderBasis.height

  46. theorem OAI.Thomason.Construction.DirectedComplex.rightCylinderMap_agree_below line 659

    Source documentation

    Agreement below a bound survives right tensoring with the interval.

    theorem rightCylinderMap_agree_below
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k < n → f.app k = g.app k) :
    ∀ k, k < n → (RightCylinder.map f).app k = (RightCylinder.map g).app k := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map

  47. theorem OAI.Thomason.Construction.DirectedComplex.rightCylinderMap_positive_degree_bridge line 668

    Source documentation

    The positive degree bridge transports through the actual signed right-cylinder differential.

    theorem rightCylinderMap_positive_degree_bridge
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k < n → f.app k = g.app k)
    (hbridge : ∀ v : K.group n, v ∈ K.positive n →
      ∃ z : L.group (n+1), z ∈ L.positive (n+1) ∧
        L.differential n z = g.app n v - f.app n v) :
    ∀ v : (rightCylinder K).group n, v ∈ (rightCylinder K).positive n →
      ∃ z : (rightCylinder L).group (n+1), z ∈ (rightCylinder L).positive (n+1) ∧
        (rightCylinder L).differential n z =
          (RightCylinder.map g).app n v - (RightCylinder.map f).app n v := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map

  48. theorem OAI.Thomason.Construction.DirectedComplex.rightCylinder_realization_comp_eq_of_positive_degree_bridge line 701

    Source documentation

    Positive bridges in the original complexes force exact equality after mapping the right-cylinder realizations into a truncated target.

    theorem rightCylinder_realization_comp_eq_of_positive_degree_bridge
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k < n → f.app k = g.app k)
    (hbridge : ∀ v : K.group n, v ∈ K.positive n →
      ∃ z : L.group (n+1), z ∈ L.positive (n+1) ∧
        L.differential n z = g.app n v - f.app n v)
    {Y : StrictOmegaCategory.{u}} (hY : Y.IsTruncated n)
    (H : (rightCylinder L).realization ⟶ Y) :
    (RightCylinder.map f).realization ≫ H = (RightCylinder.map g).realization ≫ H :=
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map

  49. abbrev OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Bounded line 735
  50. abbrev OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Free line 736
  51. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.composite line 738
  52. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Relations line 743

    Source documentation

    The defining additive relation for one actual strict composition.

    def Relations (n : ℕ) : Set (Free C n) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Free

  53. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.relations line 749
  54. abbrev OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains line 751
  55. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator line 753
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator_composite line 757

    Source documentation

    Strict composition is addition in the constructed chain group.

    theorem generator_composite {n : ℕ} (k : ℕ) (hk : k < n) (x y : Bounded C n)
    (h : C.target k x.val = C.source k y.val) :
    generator C n (composite C k hk x y h) = generator C n x + generator C n y := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Bounded, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.composite

  57. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator_identity line 772

    Source documentation

    Identity extensions have zero positive-dimensional chain.

    theorem generator_identity (n : ℕ) (x : C) (hx : C.DimensionLE n x) :
    generator C (n + 1) ⟨x, C.dimensionLE_mono (Nat.le_succ n) hx⟩ = 0 := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator

  58. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.lift line 786

    Source documentation

    The degreewise universal property, retaining every composition relation.

    def lift {A : Type*} [AddCommGroup A] (n : ℕ) (f : Bounded C n → A)
    (hf : ∀ (k : ℕ) (hk : k < n) (x y : Bounded C n)
      (h : C.target k x.val = C.source k y.val),
      f (composite C k hk x y h) = f x + f y) : Chains C n →+ A :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Bounded, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.composite, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains

  59. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.lift_generator line 797
  60. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.hom_ext line 802
  61. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator line 809

    Source documentation

    A face generator is defined with its canonical dimension witness.

    def faceGenerator (a : Bool) (n : ℕ) (x : C) : Chains C n :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains

  62. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator_composite line 812
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.boundary_composite line 827

    Source documentation

    The signed boundary respects each relation in degree n+1.

    theorem boundary_composite (n k : ℕ) (hk : k < n + 1) (x y : Bounded C (n + 1))
    (h : C.target k x.val = C.source k y.val) :
    (faceGenerator C true n (composite C k hk x y h).val -
      faceGenerator C false n (composite C k hk x y h).val) =
    (faceGenerator C true n x.val - faceGenerator C false n x.val) +
      (faceGenerator C true n y.val - faceGenerator C false n y.val) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Bounded, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.composite

  64. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.differential line 851

    Source documentation

    Differential of lambda, defined on the quotient rather than postulated.

    def differential (n : ℕ) : Chains C (n + 1) →+ Chains C n :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains

  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.differential_generator line 855
  66. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.differential_faceGenerator line 860
  67. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.faceGenerator_face line 866
  68. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.differential_squared line 872
  69. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.augmentation line 882
  70. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.augmentation_generator line 885
  71. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.augmentation_faceGenerator line 888
  72. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.augmentation_differential line 891
  73. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.positive line 901

    Source documentation

    The positive monoid consists of sums of actual cell generators.

    def positive (n : ℕ) : AddSubmonoid (Chains C n) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.Chains

  74. theorem OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.generator_positive line 904
  75. def OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex line 908

    Source documentation

    The actual augmented directed complex associated to a strict category.

    def complex : DirectedComplex.{0} where
…