OAI/Algebra/Finitistic/Rectification/SourceFiltrationCone.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExternalTensor.Section4.SourceFiltration.coneIso line 12

   Source documentation

   An isomorphism of the two input columns gives an isomorphism of actual cones.

   def coneIso {X Y X' Y' : BiComplex k B} (p : X ⟶ Y) (p' : X' ⟶ Y')
       (a : X ≅ X') (b : Y ≅ Y') (w : a.hom ≫ p' = p ≫ b.hom) :
       mappingCone p ≅ mappingCone p' where
   …

   Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.p

2. theorem OAI.ExternalTensor.Section4.SourceFiltration.zeroCone_inclusion_product line 25
3. theorem OAI.ExternalTensor.Section4.SourceFiltration.zeroCone_inclusion_bijective line 33
4. instance OAI.ExternalTensor.Section4.SourceFiltration.zeroCone_inclusion_isIso line 48
5. def OAI.ExternalTensor.Section4.SourceFiltration.twoColumnIso line 55

   Source documentation

   The ordinary two-column total identifies with the three-column API having zero relation column; its zero-column inclusion is unchanged.

   def twoColumnIso {Y : BiComplex k B} (p : X ⟶ Y)
       (h : Homotopy ((0 : Z ⟶ X) ≫ p) 0) : mappingCone p ≅ total p 0 h :=
   …

   Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.SourceFiltration.Z

6. theorem OAI.ExternalTensor.Section4.SourceFiltration.twoColumnIso_inclusion line 60
7. def OAI.ExternalTensor.Section4.SourceFiltration.f1ConeIso line 73
8. def OAI.ExternalTensor.Section4.SourceFiltration.grade1ConeIso line 75