docs: Some doc strings for instances

HepLean/Lorentz/ComplexTensor/Basic.lean

@@ -37,6 +37,7 @@ inductive Color
   | up : Color
   | down : Color
 
+/-- Color for complex Lorentz tensors is decidable. -/
 instance : DecidableEq Color := fun x y =>
   match x, y with
   | Color.upL, Color.upL => isTrue rfl

HepLean/Lorentz/Group/Basic.lean

@@ -93,6 +93,7 @@ end LorentzGroup
 
 -/
 
+/-- The instance of a group on `LorentzGroup d`. -/
 @[simps! mul_coe one_coe inv div]
 instance lorentzGroupIsGroup : Group (LorentzGroup d) where
   mul A B := ⟨A.1 * B.1, LorentzGroup.mem_mul A.2 B.2⟩
@@ -114,6 +115,7 @@ variable {Λ Λ' : LorentzGroup d}
 
 lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= (inv_eq_left_inv (mem_iff_dual_mul_self.mp Λ.2)).symm
 
+/-- The underlying matrix of a Lorentz transformation is invertible. -/
 instance (M : LorentzGroup d) : Invertible M.1 where
   invOf := M⁻¹
   invOf_mul_self := by
@@ -256,6 +258,8 @@ lemma toGL_embedding : IsEmbedding (@toGL d).toFun where
       isOpen_induced_iff]
     exact exists_exists_and_eq_and
 
+/-- The embedding of the Lorentz group into `GL(n, ℝ)` gives `LorentzGroup d` an instance
+  of a topological group. -/
 instance : TopologicalGroup (LorentzGroup d) :=
   IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing
 
@@ -281,6 +285,7 @@ def toComplex : LorentzGroup d →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
     simp only [← Matrix.map_mul, RingHom.map_matrix_mul]
     rfl
 
+/-- The image of a Lorentz transformation under `toComplex` is invertible. -/
 instance (M : LorentzGroup d) : Invertible (toComplex M) where
   invOf := toComplex M⁻¹
   invOf_mul_self := by
@@ -324,42 +329,6 @@ lemma toComplex_mulVec_ofReal (v : Fin 1 ⊕ Fin d → ℝ) (Λ : LorentzGroup d
   funext i
   rw [← RingHom.map_mulVec]
   rfl
-  /-!
-/-!
-
-# To a norm one Lorentz vector
-
--/
-
-/-- The first column of a Lorentz matrix as a `NormOneLorentzVector`. -/
-@[simps!]
-def toNormOneLorentzVector (Λ : LorentzGroup d) : NormOneLorentzVector d :=
-  ⟨Λ.1 *ᵥ timeVec, by rw [NormOneLorentzVector.mem_iff, Λ.2, minkowskiMetric.on_timeVec]⟩
-
-/-!
-
-# The time like element
-
--/
-
-/-- The time like element of a Lorentz matrix. -/
-@[simp]
-def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0)
-
-lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by
-  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  rfl
-
-lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
-    ⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by
-  simp only [timeComp, Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fintype.sum_sum_type,
-    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector,
-    transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply,
-    RCLike.inner_apply, conj_trivial]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  simp
--/
 
 /-- The parity transformation. -/
 def parity : LorentzGroup d := ⟨minkowskiMatrix, by

HepLean/Lorentz/Group/Proper.lean

@@ -30,13 +30,17 @@ lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
   refine mul_self_eq_one_iff.mp ?_
   simpa only [det_mul, det_dual, det_one] using congrArg det ((mem_iff_self_mul_dual).mp Λ.2)
 
+/-- The group `ℤ₂`. -/
 local notation "ℤ₂" => Multiplicative (ZMod 2)
 
+/-- The instance of a topological space on `ℤ₂` corresponding to the discrete topology. -/
 instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
 
+/-- The topological space defined by `ℤ₂` is discrete. -/
 instance : DiscreteTopology ℤ₂ := by
   exact forall_open_iff_discrete.mp fun _ => trivial
 
+/-- The instance of a topological group on `ℤ₂` defined via the discrete topology. -/
 instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk
 
 /-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/
@@ -138,8 +142,12 @@ def detRep : 𝓛 d →* ℤ₂ where
         apply (detContinuous_eq_one _).mpr
         simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_neg, mul_one, neg_neg]
 
+/-- The representation of the Lorentz group defined by taking the determinant `detRep` is
+  continuous. -/
 lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2
 
+/-- Two Lorentz transformations which are in the same connected component have the same
+  determinant. -/
 lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     Λ.1.det = Λ'.1.det := by
   obtain ⟨s, hs, hΛ'⟩ := h
@@ -149,12 +157,15 @@ lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connecte
     (@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2))
     (Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)
 
+/-- Two Lorentz transformations which are in the same connected component have the same
+  image under `detRep`, the determinant representation. -/
 lemma detRep_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     detRep Λ = detRep Λ' := by
   simp only [detRep_apply, detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
     coeForℤ₂_apply, Subtype.mk.injEq]
   rw [det_on_connected_component h]
 
+/-- Two Lorentz transformations which are joined by a path have the same determinant. -/
 lemma det_of_joined {Λ Λ' : LorentzGroup d} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det :=
   det_on_connected_component $ pathComponent_subset_component _ h
 
@@ -162,18 +173,24 @@ lemma det_of_joined {Λ Λ' : LorentzGroup d} (h : Joined Λ Λ') : Λ.1.det =
 @[simp]
 def IsProper (Λ : LorentzGroup d) : Prop := Λ.1.det = 1
 
+/-- The predicate `IsProper` is decidable. -/
 instance : DecidablePred (@IsProper d) := by
   intro Λ
   apply Real.decidableEq
 
+/-- A Lorentz transformation is proper if it's image under the det-representation
+  `detRep` is `1`. -/
 lemma IsProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := by
   rw [show 1 = detRep 1 from Eq.symm (MonoidHom.map_one detRep), detRep_apply, detRep_apply,
     detContinuous_eq_iff_det_eq]
   simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]
 
+/-- The identity Lorentz transformation is proper. -/
 lemma id_IsProper : @IsProper d 1 := by
   simp [IsProper]
 
+/-- If two Lorentz transformations are in the same connected componenet, and one is proper then
+  the other is also proper. -/
 lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     IsProper Λ ↔ IsProper Λ' := by
   simp only [IsProper]

HepLean/Lorentz/RealVector/Modules.lean

@@ -278,6 +278,8 @@ lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) :
 ## Topology
 -/
 
+/-- The type `ContrMod d` carries an instance of a topological group, induced by
+  it's equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
 instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced
   ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
 

HepLean/Lorentz/RealVector/NormOne.lean

@@ -36,6 +36,7 @@ lemma mem_mulAction (g : LorentzGroup d) (v : Contr d) :
     v ∈ NormOne d ↔ (Contr d).ρ g v ∈ NormOne d := by
   rw [mem_iff, mem_iff, contrContrContractField.action_tmul]
 
+/-- The instance of a topological space on `NormOne d` defined as the subspace topology. -/
 instance : TopologicalSpace (NormOne d) := instTopologicalSpaceSubtype
 
 variable (v w : NormOne d)