bump to nightly-2023-06-22-01

mathlib commit leanprover-community/mathlib@f2ad364

Mathbin/CategoryTheory/Category/PartialFun.lean

@@ -38,21 +38,25 @@ universe u
 
 variable {α β : Type _}
 
+#print PartialFun /-
 /-- The category of types equipped with partial functions. -/
 def PartialFun : Type _ :=
   Type _
 #align PartialFun PartialFun
+-/
 
 namespace PartialFun
 
 instance : CoeSort PartialFun (Type _) :=
   ⟨id⟩
 
+#print PartialFun.of /-
 /-- Turns a type into a `PartialFun`. -/
 @[nolint has_nonempty_instance]
 def of : Type _ → PartialFun :=
   id
 #align PartialFun.of PartialFun.of
+-/
 
 @[simp]
 theorem coe_of (X : Type _) : ↥(of X) = X :=
@@ -62,6 +66,7 @@ theorem coe_of (X : Type _) : ↥(of X) = X :=
 instance : Inhabited PartialFun :=
   ⟨Type _⟩
 
+#print PartialFun.largeCategory /-
 instance largeCategory : LargeCategory.{u} PartialFun
     where
   Hom := PFun
@@ -71,7 +76,9 @@ instance largeCategory : LargeCategory.{u} PartialFun
   comp_id' := @PFun.id_comp
   assoc' W X Y Z _ _ _ := (PFun.comp_assoc _ _ _).symm
 #align PartialFun.large_category PartialFun.largeCategory
+-/
 
+#print PartialFun.Iso.mk /-
 /-- Constructs a partial function isomorphism between types from an equivalence between them. -/
 @[simps]
 def Iso.mk {α β : PartialFun.{u}} (e : α ≃ β) : α ≅ β
@@ -81,20 +88,24 @@ def Iso.mk {α β : PartialFun.{u}} (e : α ≃ β) : α ≅ β
   hom_inv_id' := (PFun.coe_comp _ _).symm.trans <| congr_arg coe e.symm_comp_self
   inv_hom_id' := (PFun.coe_comp _ _).symm.trans <| congr_arg coe e.self_comp_symm
 #align PartialFun.iso.mk PartialFun.Iso.mk
+-/
 
 end PartialFun
 
+#print typeToPartialFun /-
 /-- The forgetful functor from `Type` to `PartialFun` which forgets that the maps are total. -/
 def typeToPartialFun : Type u ⥤ PartialFun
     where
   obj := id
   map := @PFun.lift
   map_comp' _ _ _ _ _ := PFun.coe_comp _ _
 #align Type_to_PartialFun typeToPartialFun
+-/
 
 instance : Faithful typeToPartialFun :=
   ⟨fun X Y => PFun.lift_injective⟩
 
+#print pointedToPartialFun /-
 /-- The functor which deletes the point of a pointed type. In return, this makes the maps partial.
 This the computable part of the equivalence `PartialFun_equiv_Pointed`. -/
 @[simps map]
@@ -117,7 +128,9 @@ def pointedToPartialFun : Pointed.{u} ⥤ PartialFun
       rintro ⟨b, _, rfl : b = _, h⟩
       exact h
 #align Pointed_to_PartialFun pointedToPartialFun
+-/
 
+#print partialFunToPointed /-
 /-- The functor which maps undefined values to a new point. This makes the maps total and creates
 pointed types. This the noncomputable part of the equivalence `PartialFun_equiv_Pointed`. It can't
 be computable because `= option.none` is decidable while the domain of a general `part` isn't. -/
@@ -131,7 +144,9 @@ noncomputable def partialFunToPointed : PartialFun ⥤ Pointed := by
       map_comp' := fun X Y Z f g =>
         Pointed.Hom.ext _ _ <| funext fun o => Option.recOn o rfl fun a => Part.bind_toOption _ _ }
 #align PartialFun_to_Pointed partialFunToPointed
+-/
 
+#print partialFunEquivPointed /-
 /-- The equivalence induced by `PartialFun_to_Pointed` and `Pointed_to_PartialFun`.
 `part.equiv_option` made functorial. -/
 @[simps]
@@ -185,7 +200,9 @@ noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed := by
               · rfl
               · exact Eq.symm (of_not_not h))
 #align PartialFun_equiv_Pointed partialFunEquivPointed
+-/
 
+#print typeToPartialFunIsoPartialFunToPointed /-
 /-- Forgetting that maps are total and making them total again by adding a point is the same as just
 adding a point. -/
 @[simps]
@@ -201,4 +218,5 @@ noncomputable def typeToPartialFunIsoPartialFunToPointed :
     Pointed.Hom.ext _ _ <|
       funext fun a => Option.recOn a rfl fun a => by convert Part.some_toOption _
 #align Type_to_PartialFun_iso_PartialFun_to_Pointed typeToPartialFunIsoPartialFunToPointed
+-/
 

Mathbin/NumberTheory/NumberField/Norm.lean

@@ -33,30 +33,39 @@ namespace RingOfIntegers
 
 variable {L : Type _} (K : Type _) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
 
+#print RingOfIntegers.norm /-
 /-- `algebra.norm` as a morphism betwen the rings of integers. -/
 @[simps]
 noncomputable def norm [IsSeparable K L] : 𝓞 L →* 𝓞 K :=
   ((Algebra.norm K).restrict (𝓞 L)).codRestrict (𝓞 K) fun x => isIntegral_norm K x.2
 #align ring_of_integers.norm RingOfIntegers.norm
+-/
 
 attribute [local instance] NumberField.ringOfIntegersAlgebra
 
+#print RingOfIntegers.coe_algebraMap_norm /-
 theorem coe_algebraMap_norm [IsSeparable K L] (x : 𝓞 L) :
     (algebraMap (𝓞 K) (𝓞 L) (norm K x) : L) = algebraMap K L (Algebra.norm K (x : L)) :=
   rfl
 #align ring_of_integers.coe_algebra_map_norm RingOfIntegers.coe_algebraMap_norm
+-/
 
+#print RingOfIntegers.coe_norm_algebraMap /-
 theorem coe_norm_algebraMap [IsSeparable K L] (x : 𝓞 K) :
     (norm K (algebraMap (𝓞 K) (𝓞 L) x) : K) = Algebra.norm K (algebraMap K L x) :=
   rfl
 #align ring_of_integers.coe_norm_algebra_map RingOfIntegers.coe_norm_algebraMap
+-/
 
+#print RingOfIntegers.norm_algebraMap /-
 theorem norm_algebraMap [IsSeparable K L] (x : 𝓞 K) :
     norm K (algebraMap (𝓞 K) (𝓞 L) x) = x ^ finrank K L := by
   rw [← Subtype.coe_inj, RingOfIntegers.coe_norm_algebraMap, Algebra.norm_algebraMap,
     SubsemiringClass.coe_pow]
 #align ring_of_integers.norm_algebra_map RingOfIntegers.norm_algebraMap
+-/
 
+#print RingOfIntegers.isUnit_norm_of_isGalois /-
 theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) ↔ IsUnit x := by
   classical
   refine' ⟨fun hx => _, IsUnit.map _⟩
@@ -76,7 +85,9 @@ theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x)
   · rw [prod_singleton, AlgEquiv.coe_refl, id]
   · rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebra_map_norm]
 #align ring_of_integers.is_unit_norm_of_is_galois RingOfIntegers.isUnit_norm_of_isGalois
+-/
 
+#print RingOfIntegers.dvd_norm /-
 /-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
 `x ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x)`. -/
 theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x) := by
@@ -88,16 +99,20 @@ theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L
   rw [coe_algebra_map_norm K x, norm_eq_prod_automorphisms]
   simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
 #align ring_of_integers.dvd_norm RingOfIntegers.dvd_norm
+-/
 
 variable (F : Type _) [Field F] [Algebra K F] [IsSeparable K F] [FiniteDimensional K F]
 
+#print RingOfIntegers.norm_norm /-
 theorem norm_norm [IsSeparable K L] [Algebra F L] [IsSeparable F L] [FiniteDimensional F L]
     [IsScalarTower K F L] (x : 𝓞 L) : norm K (norm F x) = norm K x := by
   rw [← Subtype.coe_inj, norm_apply_coe, norm_apply_coe, norm_apply_coe, Algebra.norm_norm]
 #align ring_of_integers.norm_norm RingOfIntegers.norm_norm
+-/
 
 variable {F}
 
+#print RingOfIntegers.isUnit_norm /-
 theorem isUnit_norm [CharZero K] {x : 𝓞 F} : IsUnit (norm K x) ↔ IsUnit x :=
   by
   letI : Algebra K (AlgebraicClosure K) := AlgebraicClosure.algebra K
@@ -116,6 +131,7 @@ theorem isUnit_norm [CharZero K] {x : 𝓞 F} : IsUnit (norm K x) ↔ IsUnit x :
     _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
     _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)
 #align ring_of_integers.is_unit_norm RingOfIntegers.isUnit_norm
+-/
 
 end RingOfIntegers
 

Mathbin/RingTheory/Valuation/RamificationGroup.lean

@@ -26,21 +26,26 @@ open scoped Pointwise
 
 variable (K : Type _) {L : Type _} [Field K] [Field L] [Algebra K L]
 
+#print ValuationSubring.decompositionSubgroup /-
 /-- The decomposition subgroup defined as the stabilizer of the action
 on the type of all valuation subrings of the field. -/
 @[reducible]
 def decompositionSubgroup (A : ValuationSubring L) : Subgroup (L ≃ₐ[K] L) :=
   MulAction.stabilizer (L ≃ₐ[K] L) A
 #align valuation_subring.decomposition_subgroup ValuationSubring.decompositionSubgroup
+-/
 
+#print ValuationSubring.subMulAction /-
 /-- The valuation subring `A` (considered as a subset of `L`)
 is stable under the action of the decomposition group. -/
 def subMulAction (A : ValuationSubring L) : SubMulAction (A.decompositionSubgroup K) L
     where
   carrier := A
   smul_mem' g l h := Set.mem_of_mem_of_subset (Set.smul_mem_smul_set h) g.Prop.le
 #align valuation_subring.sub_mul_action ValuationSubring.subMulAction
+-/
 
+#print ValuationSubring.decompositionSubgroupMulSemiringAction /-
 /-- The multiplicative action of the decomposition subgroup on `A`. -/
 instance decompositionSubgroupMulSemiringAction (A : ValuationSubring L) :
     MulSemiringAction (A.decompositionSubgroup K) A :=
@@ -53,13 +58,16 @@ instance decompositionSubgroupMulSemiringAction (A : ValuationSubring L) :
     smul_one := fun g => Subtype.ext <| smul_one g
     smul_mul := fun g k l => Subtype.ext <| smul_mul' g k l }
 #align valuation_subring.decomposition_subgroup_mul_semiring_action ValuationSubring.decompositionSubgroupMulSemiringAction
+-/
 
+#print ValuationSubring.inertiaSubgroup /-
 /-- The inertia subgroup defined as the kernel of the group homomorphism from
 the decomposition subgroup to the group of automorphisms of the residue field of `A`. -/
 def inertiaSubgroup (A : ValuationSubring L) : Subgroup (A.decompositionSubgroup K) :=
   MonoidHom.ker <|
     MulSemiringAction.toRingAut (A.decompositionSubgroup K) (LocalRing.ResidueField A)
 #align valuation_subring.inertia_subgroup ValuationSubring.inertiaSubgroup
+-/
 
 end ValuationSubring
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "a1fd69c0ae3540f5b683423747edeb32e9046aaa",
+    "rev": "579046f06237c4d1605bcea7afa0314cf3d1c9d1",
     "name": "lean3port",
-    "inputRev?": "a1fd69c0ae3540f5b683423747edeb32e9046aaa"}},
+    "inputRev?": "579046f06237c4d1605bcea7afa0314cf3d1c9d1"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "28cbaf7d43de64040cdeb1a4b1b5622c4c3049d2",
+    "rev": "e032d377ed49c156097c62854d9dacfebe2de51b",
     "name": "mathlib",
-    "inputRev?": "28cbaf7d43de64040cdeb1a4b1b5622c4c3049d2"}},
+    "inputRev?": "e032d377ed49c156097c62854d9dacfebe2de51b"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-21-23"
+def tag : String := "nightly-2023-06-22-01"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a1fd69c0ae3540f5b683423747edeb32e9046aaa"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"579046f06237c4d1605bcea7afa0314cf3d1c9d1"
 
 @[default_target]
 lean_lib Mathbin where