Commit 2024-07-17 21:45 a365570f

View on Github →

feat(Algebra/Homology): boundaries of embeddings of complex shapes (#14650) In this PR, we define the lower/upper boundaries of embeddings of complex shapes. These notions shall be important when constructing canonical truncations of homological complexes.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/ComplexShape.lean

added theorem ComplexShape.next_eq_self'

added theorem ComplexShape.next_eq_self

added theorem ComplexShape.prev_eq_self'

added theorem ComplexShape.prev_eq_self

Modified Mathlib/Algebra/Homology/Embedding/Basic.lean

added theorem ComplexShape.Embedding.mem_next

added theorem ComplexShape.Embedding.mem_prev

Created Mathlib/Algebra/Homology/Embedding/Boundary.lean

added theorem ComplexShape.Embedding.BoundaryGE.false

added theorem ComplexShape.Embedding.BoundaryGE.not_mem

added def ComplexShape.Embedding.BoundaryGE

added theorem ComplexShape.Embedding.BoundaryLE.false

added theorem ComplexShape.Embedding.BoundaryLE.not_mem

added def ComplexShape.Embedding.BoundaryLE

added theorem ComplexShape.Embedding.boundaryGE

added theorem ComplexShape.Embedding.boundaryLE

added theorem ComplexShape.Embedding.next_f_of_not_boundaryLE

added theorem ComplexShape.Embedding.not_boundaryGE_next'

added theorem ComplexShape.Embedding.not_boundaryGE_next

added theorem ComplexShape.Embedding.not_boundaryLE_prev'

added theorem ComplexShape.Embedding.not_boundaryLE_prev

added theorem ComplexShape.Embedding.prev_f_of_not_boundaryGE

added theorem ComplexShape.boundaryGE_embeddingUpIntGE_iff

added theorem ComplexShape.boundaryLE_embeddingUpIntLE_iff