[Merged by Bors] - doc: fix diagram formatting

Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

@@ -116,11 +116,13 @@ set_option maxHeartbeats 400000 in
 /-- This iso witnesses the fact that
 given `f : X ⟶ Y`, `i : U ⟶ Y`, and `i₁ : V₁ ⟶ X ×[Y] U`, `i₂ : V₂ ⟶ X ×[Y] U`, the diagram
 
+```
 V₁ ×[X ×[Y] U] V₂ ⟶ V₁ ×[U] V₂
         |                 |
         |                 |
         ↓                 ↓
-        X        ⟶ X ×[Y] X
+        X         ⟶   X ×[Y] X
+```
 
 is a pullback square.
 Also see `pullback_fst_map_snd_isPullback`.
@@ -207,11 +209,13 @@ variable
 /-- This iso witnesses the fact that
 given `f : X ⟶ T`, `g : Y ⟶ T`, and `i : T ⟶ S`, the diagram
 
+```
 X ×ₜ Y ⟶ X ×ₛ Y
   |         |
   |         |
   ↓         ↓
-  T  ⟶  T ×ₛ T
+  T    ⟶  T ×ₛ T
+```
 
 is a pullback square.
 Also see `pullback_map_diagonal_isPullback`.
@@ -363,19 +367,23 @@ end
 
 /-- Given the following diagram with `S ⟶ S'` a monomorphism,
 
+```
     X ⟶ X'
       ↘      ↘
         S ⟶ S'
       ↗      ↗
     Y ⟶ Y'
+```
 
 This iso witnesses the fact that
 
+```
       X ×[S] Y ⟶ (X' ×[S'] Y') ×[Y'] Y
           |                  |
           |                  |
           ↓                  ↓
 (X' ×[S'] Y') ×[X'] X ⟶ X' ×[S'] Y'
+```
 
 is a pullback square. The diagonal map of this square is `pullback.map`.
 Also see `pullback_lift_map_is_pullback`.

Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

@@ -37,9 +37,11 @@ variable {C : Type u} [Category.{v} C]
 
 /-- Given any pullback diagram of the form
 
-Z ⟶ X₁
-↓      ↓
+```
+Z  ⟶ X₁
+↓    ↓
 X₂ ⟶ X
+```
 
 where `X₁ ⟶ X ← X₂` is a coproduct diagram, then `Z` is initial, and both `X₁ ⟶ X` and `X₂ ⟶ X`
 are mono.
@@ -55,9 +57,11 @@ class CoproductDisjoint (X₁ X₂ : C) where
 
 /-- If the coproduct of `X₁` and `X₂` is disjoint, then given any pullback square
 
-Z ⟶ X₁
-↓      ↓
+```
+Z  ⟶ X₁
+↓    ↓
 X₂ ⟶ X
+```
 
 where `X₁ ⟶ X ← X₂` is a coproduct, then `Z` is initial.
 -/
@@ -69,9 +73,11 @@ def isInitialOfIsPullbackOfIsCoproduct {Z X₁ X₂ X : C} [CoproductDisjoint X
 
 /-- If the coproduct of `X₁` and `X₂` is disjoint, then given any pullback square
 
-Z ⟶ X₁
+```
+Z  ⟶    X₁
 ↓       ↓
 X₂ ⟶ X₁ ⨿ X₂
+```
 
 `Z` is initial.
 -/
@@ -85,9 +91,11 @@ noncomputable def isInitialOfIsPullbackOfCoproduct {Z X₁ X₂ : C} [HasBinaryC
 /-- If the coproduct of `X₁` and `X₂` is disjoint, then provided `X₁ ⟶ X ← X₂` is a coproduct the
 pullback is an initial object:
 
-        X₁
-        ↓
+```
+     X₁
+     ↓
 X₂ ⟶ X
+```
 -/
 noncomputable def isInitialOfPullbackOfIsCoproduct {X X₁ X₂ : C} [CoproductDisjoint X₁ X₂]
     {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} [HasPullback pX₁ pX₂] (cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) :

Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean

@@ -29,7 +29,7 @@ section PullbackAssoc
 
 /-
 The objects and morphisms are as follows:
-
+```
            Z₂ - g₄ -> X₃
            |          |
            g₃         f₄
@@ -39,19 +39,23 @@ Z₁ - g₂ -> X₂ - f₃ -> Y₂
 g₁         f₂
 ∨          ∨
 X₁ - f₁ -> Y₁
+```
 
 where the two squares are pullbacks.
 
 We can then construct the pullback squares
 
+```
 W  - l₂ -> Z₂ - g₄ -> X₃
 |                     |
 l₁                    f₄
 ∨                     ∨
 Z₁ - g₂ -> X₂ - f₃ -> Y₂
+```
 
 and
 
+```
 W' - l₂' -> Z₂
 |           |
 l₁'         g₃
@@ -61,6 +65,7 @@ Z₁          X₂
 g₁          f₂
 ∨           ∨
 X₁ -  f₁ -> Y₁
+```
 
 We will show that both `W` and `W'` are pullbacks over `g₁, g₂`, and thus we may construct a
 canonical isomorphism between them. -/
@@ -228,6 +233,7 @@ section PushoutAssoc
 /-
 The objects and morphisms are as follows:
 
+```
            Z₂ - g₄ -> X₃
            |          |
            g₃         f₄
@@ -237,11 +243,13 @@ Z₁ - g₂ -> X₂ - f₃ -> Y₂
 g₁         f₂
 ∨          ∨
 X₁ - f₁ -> Y₁
+```
 
 where the two squares are pushouts.
 
 We can then construct the pushout squares
 
+```
 Z₁ - g₂ -> X₂ - f₃ -> Y₂
 |                     |
 g₁                    l₂
@@ -259,6 +267,7 @@ X₂          Y₂
 f₂          l₂'
 ∨           ∨
 Y₁ - l₁' -> W'
+```
 
 We will show that both `W` and `W'` are pushouts over `f₂, f₃`, and thus we may construct a
 canonical isomorphism between them. -/

Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

@@ -214,12 +214,13 @@ theorem pushout.condition {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f
 
 /-- Given such a diagram, then there is a natural morphism `W ×ₛ X ⟶ Y ×ₜ Z`.
 
-    W ⟶ Y
-      ↘      ↘
-        S ⟶ T
-      ↗      ↗
-    X ⟶ Z
-
+```
+W ⟶ Y
+  ↘   ↘
+  S ⟶ T
+  ↗   ↗
+X ⟶ Z
+```
 -/
 abbrev pullback.map {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [HasPullback f₁ f₂] (g₁ : Y ⟶ T)
     (g₂ : Z ⟶ T) [HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
@@ -236,12 +237,13 @@ abbrev pullback.mapDesc {X Y S T : C} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T)
 
 /-- Given such a diagram, then there is a natural morphism `W ⨿ₛ X ⟶ Y ⨿ₜ Z`.
 
-        W ⟶ Y
-      ↗      ↗
-    S ⟶ T
-      ↘      ↘
-        X ⟶ Z
-
+```
+  W ⟶ Y
+ ↗   ↗
+S ⟶ T
+ ↘   ↘
+  X ⟶ Z
+```
 -/
 abbrev pushout.map {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X) [HasPushout f₁ f₂] (g₁ : T ⟶ Y)
     (g₂ : T ⟶ Z) [HasPushout g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁)

Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean

@@ -46,11 +46,13 @@ variable (h₁ : i₁ ≫ g₁ = f₁ ≫ i₂) (h₂ : i₂ ≫ g₂ = f₂ ≫
 
 /-- Given
 
+```
 X₁ - f₁ -> X₂ - f₂ -> X₃
 |          |          |
 i₁         i₂         i₃
-∨          ∨          ∨
+↓          ↓          ↓
 Y₁ - g₁ -> Y₂ - g₂ -> Y₃
+```
 
 Then the big square is a pullback if both the small squares are.
 -/
@@ -82,11 +84,13 @@ def bigSquareIsPullback (H : IsLimit (PullbackCone.mk _ _ h₂))
 
 /-- Given
 
+```
 X₁ - f₁ -> X₂ - f₂ -> X₃
 |          |          |
 i₁         i₂         i₃
-∨          ∨          ∨
+↓          ↓          ↓
 Y₁ - g₁ -> Y₂ - g₂ -> Y₃
+```
 
 Then the big square is a pushout if both the small squares are.
 -/
@@ -119,11 +123,13 @@ def bigSquareIsPushout (H : IsColimit (PushoutCocone.mk _ _ h₂))
 
 /-- Given
 
+```
 X₁ - f₁ -> X₂ - f₂ -> X₃
 |          |          |
 i₁         i₂         i₃
-∨          ∨          ∨
+↓          ↓          ↓
 Y₁ - g₁ -> Y₂ - g₂ -> Y₃
+```
 
 Then the left square is a pullback if the right square and the big square are.
 -/
@@ -156,11 +162,13 @@ def leftSquareIsPullback (H : IsLimit (PullbackCone.mk _ _ h₂))
 
 /-- Given
 
+```
 X₁ - f₁ -> X₂ - f₂ -> X₃
 |          |          |
 i₁         i₂         i₃
-∨          ∨          ∨
+↓          ↓          ↓
 Y₁ - g₁ -> Y₂ - g₂ -> Y₃
+```
 
 Then the right square is a pushout if the left square and the big square are.
 -/

Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean

@@ -39,14 +39,18 @@ variable {X Y : C} (f g : X ⟶ Y)
 
 /-- A split equalizer diagram consists of morphisms
 
+```
       ι   f
     W → X ⇉ Y
           g
+```
 
 satisfying `ι ≫ f = ι ≫ g` together with morphisms
 
+```
       r   t
     W ← X ← Y
+```
 
 satisfying `ι ≫ r = 𝟙 W`, `g ≫ t = 𝟙 X` and `f ≫ t = r ≫ ι`.
 

Mathlib/RingTheory/Etale/Basic.lean

@@ -128,11 +128,13 @@ section Localization
 
 We now consider a commutative square of commutative rings
 
+```
 R -----> S
 |        |
 |        |
 v        v
 Rₘ ----> Sₘ
+```
 
 where `Rₘ` and `Sₘ` are the localisations of `R` and `S` at a multiplicatively closed
 subset `M` of `R`.

Mathlib/RingTheory/Kaehler/Basic.lean

@@ -614,10 +614,13 @@ end Presentation
 section ExactSequence
 
 /- We have the commutative diagram
+```
 A --→ B
 ↑     ↑
 |     |
-R --→ S -/
+R --→ S
+```
+-/
 variable (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 variable [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B]
 variable [SMulCommClass S A B]
@@ -630,10 +633,12 @@ local macro "finsupp_map" : term =>
 
 /--
 Given the commutative diagram
+```
 A --→ B
 ↑     ↑
 |     |
 R --→ S
+```
 The kernel of the presentation `⊕ₓ B dx ↠ Ω_{B/S}` is spanned by the image of the
 kernel of `⊕ₓ A dx ↠ Ω_{A/R}` and all `ds` with `s : S`.
 See `kerTotal_map'` for the special case where `R = S`.
@@ -675,10 +680,13 @@ theorem KaehlerDifferential.kerTotal_map' (h : Function.Surjective (algebraMap A
   ext; simp [IsScalarTower.algebraMap_eq R A B]
 
 /-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄S]` given a square
+```
 A --→ B
 ↑     ↑
 |     |
-R --→ S -/
+R --→ S
+```
+-/
 def KaehlerDifferential.map : Ω[A⁄R] →ₗ[A] Ω[B⁄S] :=
   Derivation.liftKaehlerDifferential
     (((KaehlerDifferential.D S B).restrictScalars R).compAlgebraMap A)

Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

@@ -274,11 +274,13 @@ theorem pullback_snd_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
 /-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are embeddings,
 then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an embedding.
 
-  W ⟶ Y
-    ↘      ↘
-      S ⟶ T
-    ↗      ↗
-  X ⟶ Z
+```
+W ⟶ Y
+ ↘   ↘
+  S ⟶ T
+ ↗   ↗
+X ⟶ Z
+```
 -/
 theorem pullback_map_embedding_of_embeddings {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) (f₂ : X ⟶ S)
     (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Embedding i₁) (H₂ : Embedding i₂)
@@ -298,11 +300,14 @@ theorem pullback_map_embedding_of_embeddings {W X Y Z S T : TopCat.{u}} (f₁ :
 
 /-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are open embeddings, and `S ⟶ T`
 is mono, then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an open embedding.
-  W ⟶ Y
-    ↘      ↘
-      S ⟶ T
-    ↗       ↗
-  X ⟶ Z
+
+```
+W ⟶ Y
+ ↘   ↘
+  S ⟶ T
+ ↗   ↗
+X ⟶ Z
+```
 -/
 theorem pullback_map_openEmbedding_of_open_embeddings {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S)
     (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : OpenEmbedding i₁)