From 70450a3cdba0521339ab92bdbcdb925ff387f506 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Fri, 23 Jun 2023 07:06:52 +0000 Subject: [PATCH] bump to nightly-2023-06-23-07 mathlib commit https://github.com/leanprover-community/mathlib/commit/d30d31261cdb4d2f5e612eabc3c4bf45556350d5 --- .../PresheafedSpace/Gluing.lean | 72 +++++++++++++++++++ Mathbin/Geometry/Manifold/Sheaf/Basic.lean | 12 ++++ .../CliffordAlgebra/Grading.lean | 34 +++++++++ .../NumberTheory/Cyclotomic/Discriminant.lean | 12 ++++ lake-manifest.json | 8 +-- lakefile.lean | 4 +- 6 files changed, 136 insertions(+), 6 deletions(-) diff --git a/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean b/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean index c142fc9f30..8d1c59c033 100644 --- a/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean +++ b/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean @@ -75,6 +75,7 @@ variable (C : Type u) [Category.{v} C] namespace PresheafedSpace +#print AlgebraicGeometry.PresheafedSpace.GlueData /- /-- A family of gluing data consists of 1. An index type `J` 2. A presheafed space `U i` for each `i : J`. @@ -97,6 +98,7 @@ that the `U i`'s are open subspaces of the glued space. structure GlueData extends GlueData (PresheafedSpace.{v} C) where f_open : ∀ i j, IsOpenImmersion (f i j) #align algebraic_geometry.PresheafedSpace.glue_data AlgebraicGeometry.PresheafedSpace.GlueData +-/ attribute [instance] glue_data.f_open @@ -116,12 +118,15 @@ local notation "π₁⁻¹ " i ", " j ", " k => local notation "π₂⁻¹ " i ", " j ", " k => (PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft (D.f i j) (D.f i k)).invApp +#print AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData /- /-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces. -/ abbrev toTopGlueData : TopCat.GlueData := { f_open := fun i j => (D.f_open i j).base_open toGlueData := 𝖣.mapGlueData (forget C) } #align algebraic_geometry.PresheafedSpace.glue_data.to_Top_glue_data AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding /- theorem ι_openEmbedding [HasLimits C] (i : D.J) : OpenEmbedding (𝖣.ι i).base := by rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _] @@ -130,7 +135,9 @@ theorem ι_openEmbedding [HasLimits C] (i : D.J) : OpenEmbedding (𝖣.ι i).bas (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).OpenEmbedding (D.to_Top_glue_data.ι_open_embedding i) #align algebraic_geometry.PresheafedSpace.glue_data.ι_open_embedding AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base /- theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) : (π₂ i, j, k) '' ((π₁ i, j, k) ⁻¹' S) = D.f i k ⁻¹' (D.f i j '' S) := by @@ -142,7 +149,9 @@ theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) : rw [← TopCat.epi_iff_surjective] infer_instance #align algebraic_geometry.PresheafedSpace.glue_data.pullback_base AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app /- /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute. -/ @[simp, reassoc] theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) : @@ -169,7 +178,9 @@ theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) : erw [(D.V (i, k)).Presheaf.map_id] rfl #align algebraic_geometry.PresheafedSpace.glue_data.f_inv_app_f_app AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' /- /-- We can prove the `eq` along with the lemma. Thus this is bundled together here, and the lemma itself is separated below. -/ @@ -199,7 +210,9 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k) congr 2 rw [is_iso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, category.comp_id] #align algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app' AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app /- /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/q6X1GJ9.png) commute. -/ @[simp, reassoc] theorem snd_invApp_t_app (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)).carrier) : @@ -213,9 +226,11 @@ theorem snd_invApp_t_app (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)) rw [← e] simp [eq_to_hom_map] #align algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app +-/ variable [HasLimits C] +#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq /- theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) : (Opens.map (𝖣.ι j).base).obj ((D.ι_openEmbedding i).IsOpenMap.Functor.obj U) = (D.f_open j i).openFunctor.obj @@ -240,7 +255,9 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) : · rw [← TopCat.mono_iff_injective] infer_instance #align algebraic_geometry.PresheafedSpace.glue_data.ι_image_preimage_eq AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap /- /-- (Implementation). The map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' (𝖣.ι i '' U))` -/ def opensImagePreimageMap (i j : D.J) (U : Opens (D.U i).carrier) : (D.U i).Presheaf.obj (op U) ⟶ (D.U j).Presheaf.obj _ := @@ -249,7 +266,9 @@ def opensImagePreimageMap (i j : D.J) (U : Opens (D.U i).carrier) : (D.f_open j i).invApp (unop _) ≫ (𝖣.U j).Presheaf.map (eqToHom (D.ι_image_preimage_eq i j U)).op #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' /- theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) : ∃ eq, D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ = @@ -268,7 +287,9 @@ theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) : rw [eq_to_hom_map (opens.map _), eq_to_hom_op, eq_to_hom_trans] congr #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app' AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app /- /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/mBzV1Rx.png) commute. -/ theorem opensImagePreimageMap_app (i j k : D.J) (U : Opens (D.U i).carrier) : D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ = @@ -277,7 +298,9 @@ theorem opensImagePreimageMap_app (i j k : D.J) (U : Opens (D.U i).carrier) : (D.V (j, k)).Presheaf.map (eqToHom (opensImagePreimageMap_app' D i j k U).some) := (opensImagePreimageMap_app' D i j k U).choose_spec #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc /- -- This is proved separately since `reassoc` somehow timeouts. theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier) {X' : C} (f' : _ ⟶ X') : @@ -289,19 +312,25 @@ theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier simpa only [category.assoc] using congr_arg (fun g => g ≫ f') (opens_image_preimage_map_app D i j k U) #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app_assoc AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen /- /-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of the image `ι '' U` in the glued space is the limit of this diagram. -/ abbrev diagramOverOpen {i : D.J} (U : Opens (D.U i).carrier) : (WalkingMultispan _ _)ᵒᵖ ⥤ C := componentwiseDiagram 𝖣.diagram.multispan ((D.ι_openEmbedding i).IsOpenMap.Functor.obj U) #align algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ /- /-- (Implementation) The projection from the limit of `diagram_over_open` to a component of `D.U j`. -/ abbrev diagramOverOpenπ {i : D.J} (U : Opens (D.U i).carrier) (j : D.J) := limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) #align algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open_π AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp /- /-- (Implementation) We construct the map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V)` for each `V` in the gluing diagram. We will lift these maps into `ι_inv_app`. -/ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) : @@ -319,7 +348,9 @@ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) : exact colimit.w 𝖣.diagram.multispan (walking_multispan.hom.fst (j, k)) · exact D.opens_image_preimage_map i j U #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp /- /-- (Implementation) The natural map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, 𝖣.ι i '' U)`. This forms the inverse of `(𝖣.ι i).c.app (op U)`. -/ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) : @@ -373,7 +404,9 @@ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) : repeat' erw [← (D.V (j, k)).Presheaf.map_comp] congr } } #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π /- /-- `ι_inv_app` is the left inverse of `D.ι i` on `U`. -/ theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) : ∃ eq, D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).Presheaf.map (eqToHom Eq) := @@ -391,12 +424,16 @@ theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) : · rw [← TopCat.epi_iff_surjective] infer_instance #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap /- /-- The `eq_to_hom` given by `ι_inv_app_π`. -/ abbrev ιInvAppπEqMap {i : D.J} (U : Opens (D.U i).carrier) := (D.U i).Presheaf.map (eqToIso (D.ιInvApp_π U).some).inv #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_eq_map AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π /- /-- `ι_inv_app` is the right inverse of `D.ι i` on `U`. -/ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = @@ -430,7 +467,9 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) : erw [D.ι_image_preimage_eq i j U] all_goals infer_instance #align algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_π AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id /- /-- `ι_inv_app` is the inverse of `D.ι i` on `U`. -/ theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 _ := @@ -449,7 +488,11 @@ theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) : rw [category.id_comp] apply π_ι_inv_app_π #align algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_eq_id AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id +-/ +/- warning: algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso clashes with algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_IsIso -> AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso +Case conversion may be inaccurate. Consider using '#align algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIsoₓ'. -/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso /- instance componentwise_diagram_π_isIso (i : D.J) (U : Opens (D.U i).carrier) : IsIso (D.diagramOverOpenπ U i) := by @@ -459,13 +502,19 @@ instance componentwise_diagram_π_isIso (i : D.J) (U : Opens (D.U i).carrier) : · rw [category.assoc, (D.ι_inv_app_π _).choose_spec] exact iso.inv_hom_id ((D.to_glue_data.U i).Presheaf.mapIso (eq_to_iso _)) #align algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso +-/ +/- warning: algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.PresheafedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion +Case conversion may be inaccurate. Consider using '#align algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersionₓ'. -/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion /- instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) where base_open := D.ι_openEmbedding i c_iso U := by erw [← colimit_presheaf_obj_iso_componentwise_limit_hom_π]; infer_instance #align algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit /- /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`. Vᵢⱼ ⟶ Uᵢ @@ -497,10 +546,13 @@ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) := erw [is_open_immersion.lift_fac_assoc] · intro m e₁ e₂; rw [← cancel_mono (D.f i j)]; erw [e₁]; rw [is_open_immersion.lift_fac] #align algebraic_geometry.PresheafedSpace.glue_data.V_pullback_cone_is_limit AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit +-/ +#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective /- theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x := 𝖣.ι_jointly_surjective (PresheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x #align algebraic_geometry.PresheafedSpace.glue_data.ι_jointly_surjective AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective +-/ end GlueData @@ -560,9 +612,13 @@ theorem ι_isoPresheafedSpace_inv (i : D.J) : 𝖣.ι_gluedIso_inv _ _ #align algebraic_geometry.SheafedSpace.glue_data.ι_iso_PresheafedSpace_inv AlgebraicGeometry.SheafedSpaceₓ.GlueData.ι_isoPresheafedSpace_inv +/- warning: algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.SheafedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion +Case conversion may be inaccurate. Consider using '#align algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersionₓ'. -/ +#print AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion /- instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) := by rw [← D.ι_iso_PresheafedSpace_inv]; infer_instance #align algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion +-/ theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x := 𝖣.ι_jointly_surjective (SheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x @@ -586,6 +642,7 @@ end SheafedSpace namespace LocallyRingedSpace +#print AlgebraicGeometry.LocallyRingedSpace.GlueData /- /-- A family of gluing data consists of 1. An index type `J` 2. A locally ringed space `U i` for each `i : J`. @@ -608,6 +665,7 @@ that the `U i`'s are open subspaces of the glued space. structure GlueData extends GlueData LocallyRingedSpace where f_open : ∀ i j, LocallyRingedSpace.IsOpenImmersion (f i j) #align algebraic_geometry.LocallyRingedSpace.glue_data AlgebraicGeometry.LocallyRingedSpace.GlueData +-/ attribute [instance] glue_data.f_open @@ -617,36 +675,49 @@ variable (D : GlueData) local notation "𝖣" => D.toGlueData +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData /- /-- The glue data of ringed spaces associated to a family of glue data of locally ringed spaces. -/ abbrev toSheafedSpaceGlueData : SheafedSpace.GlueData CommRingCat := { f_open := D.f_open toGlueData := 𝖣.mapGlueData forgetToSheafedSpace } #align algebraic_geometry.LocallyRingedSpace.glue_data.to_SheafedSpace_glue_data AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData +-/ +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace /- /-- The gluing as locally ringed spaces is isomorphic to the gluing as ringed spaces. -/ abbrev isoSheafedSpace : 𝖣.glued.toSheafedSpace ≅ D.toSheafedSpaceGlueData.toGlueData.glued := 𝖣.gluedIso forgetToSheafedSpace #align algebraic_geometry.LocallyRingedSpace.glue_data.iso_SheafedSpace AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace +-/ +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv /- theorem ι_isoSheafedSpace_inv (i : D.J) : D.toSheafedSpaceGlueData.toGlueData.ι i ≫ D.isoSheafedSpace.inv = (𝖣.ι i).1 := 𝖣.ι_gluedIso_inv forgetToSheafedSpace i #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_iso_SheafedSpace_inv AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv +-/ +/- warning: algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.LocallyRingedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion +Case conversion may be inaccurate. Consider using '#align algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersionₓ'. -/ +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion /- instance ι_isOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) := by delta is_open_immersion; rw [← D.ι_iso_SheafedSpace_inv] apply PresheafedSpace.is_open_immersion.comp #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion +-/ instance (i j k : D.J) : PreservesLimit (cospan (𝖣.f i j) (𝖣.f i k)) forgetToSheafedSpace := inferInstance +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective /- theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).1.base y = x := 𝖣.ι_jointly_surjective ((LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) ⋙ forget TopCat) x #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_jointly_surjective AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective +-/ +#print AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit /- /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`. Vᵢⱼ ⟶ Uᵢ @@ -658,6 +729,7 @@ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) := 𝖣.vPullbackConeIsLimitOfMap forgetToSheafedSpace i j (D.toSheafedSpaceGlueData.vPullbackConeIsLimit _ _) #align algebraic_geometry.LocallyRingedSpace.glue_data.V_pullback_cone_is_limit AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit +-/ end GlueData diff --git a/Mathbin/Geometry/Manifold/Sheaf/Basic.lean b/Mathbin/Geometry/Manifold/Sheaf/Basic.lean index 538569b4ae..75b5d72482 100644 --- a/Mathbin/Geometry/Manifold/Sheaf/Basic.lean +++ b/Mathbin/Geometry/Manifold/Sheaf/Basic.lean @@ -45,14 +45,19 @@ variable {H : Type _} [TopologicalSpace H] {H' : Type _} [TopologicalSpace H'] (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] +#print TopCat.of.chartedSpace /- instance TopCat.of.chartedSpace : ChartedSpace H (TopCat.of M) := (inferInstance : ChartedSpace H M) #align Top.of.charted_space TopCat.of.chartedSpace +-/ +#print TopCat.of.hasGroupoid /- instance TopCat.of.hasGroupoid [HasGroupoid M G] : HasGroupoid (TopCat.of M) G := (inferInstance : HasGroupoid M G) #align Top.of.has_groupoid TopCat.of.hasGroupoid +-/ +#print StructureGroupoid.LocalInvariantProp.localPredicate /- /-- Let `P` be a `local_invariant_prop` for functions between spaces with the groupoids `G`, `G'` and let `M`, `M'` be charted spaces modelled on the model spaces of those groupoids. Then there is an induced `local_predicate` on the functions from `M` to `M'`, given by `lift_prop P`. -/ @@ -79,7 +84,9 @@ def StructureGroupoid.LocalInvariantProp.localPredicate (hG : LocalInvariantProp ext1 rfl #align structure_groupoid.local_invariant_prop.local_predicate StructureGroupoid.LocalInvariantProp.localPredicate +-/ +#print StructureGroupoid.LocalInvariantProp.sheaf /- /-- Let `P` be a `local_invariant_prop` for functions between spaces with the groupoids `G`, `G'` and let `M`, `M'` be charted spaces modelled on the model spaces of those groupoids. Then there is a sheaf of types on `M` which, to each open set `U` in `M`, associates the type of bundled @@ -88,14 +95,19 @@ def StructureGroupoid.LocalInvariantProp.sheaf (hG : LocalInvariantProp G G' P) TopCat.Sheaf (Type u) (TopCat.of M) := TopCat.subsheafToTypes (hG.LocalPredicateₓ M M') #align structure_groupoid.local_invariant_prop.sheaf StructureGroupoid.LocalInvariantProp.sheaf +-/ +#print StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun /- instance StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun (hG : LocalInvariantProp G G' P) (U : (Opens (TopCat.of M))ᵒᵖ) : CoeFun ((hG.Sheaf M M').val.obj U) fun _ => unop U → M' where coe a := a.1 #align structure_groupoid.local_invariant_prop.sheaf_has_coe_to_fun StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun +-/ +#print StructureGroupoid.LocalInvariantProp.section_spec /- theorem StructureGroupoid.LocalInvariantProp.section_spec (hG : LocalInvariantProp G G' P) (U : (Opens (TopCat.of M))ᵒᵖ) (f : (hG.Sheaf M M').val.obj U) : LiftProp P f := f.2 #align structure_groupoid.local_invariant_prop.section_spec StructureGroupoid.LocalInvariantProp.section_spec +-/ diff --git a/Mathbin/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathbin/LinearAlgebra/CliffordAlgebra/Grading.lean index 9daa0294ea..cbf04c4f4f 100644 --- a/Mathbin/LinearAlgebra/CliffordAlgebra/Grading.lean +++ b/Mathbin/LinearAlgebra/CliffordAlgebra/Grading.lean @@ -30,28 +30,37 @@ open scoped DirectSum variable (Q) +#print CliffordAlgebra.evenOdd /- /-- The even or odd submodule, defined as the supremum of the even or odd powers of `(ι Q).range`. `even_odd 0` is the even submodule, and `even_odd 1` is the odd submodule. -/ def evenOdd (i : ZMod 2) : Submodule R (CliffordAlgebra Q) := ⨆ j : { n : ℕ // ↑n = i }, (ι Q).range ^ (j : ℕ) #align clifford_algebra.even_odd CliffordAlgebra.evenOdd +-/ +#print CliffordAlgebra.one_le_evenOdd_zero /- theorem one_le_evenOdd_zero : 1 ≤ evenOdd Q 0 := by refine' le_trans _ (le_iSup _ ⟨0, Nat.cast_zero⟩) exact (pow_zero _).ge #align clifford_algebra.one_le_even_odd_zero CliffordAlgebra.one_le_evenOdd_zero +-/ +#print CliffordAlgebra.range_ι_le_evenOdd_one /- theorem range_ι_le_evenOdd_one : (ι Q).range ≤ evenOdd Q 1 := by refine' le_trans _ (le_iSup _ ⟨1, Nat.cast_one⟩) exact (pow_one _).ge #align clifford_algebra.range_ι_le_even_odd_one CliffordAlgebra.range_ι_le_evenOdd_one +-/ +#print CliffordAlgebra.ι_mem_evenOdd_one /- theorem ι_mem_evenOdd_one (m : M) : ι Q m ∈ evenOdd Q 1 := range_ι_le_evenOdd_one Q <| LinearMap.mem_range_self _ m #align clifford_algebra.ι_mem_even_odd_one CliffordAlgebra.ι_mem_evenOdd_one +-/ +#print CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero /- theorem ι_mul_ι_mem_evenOdd_zero (m₁ m₂ : M) : ι Q m₁ * ι Q m₂ ∈ evenOdd Q 0 := Submodule.mem_iSup_of_mem ⟨2, rfl⟩ (by @@ -60,7 +69,9 @@ theorem ι_mul_ι_mem_evenOdd_zero (m₁ m₂ : M) : ι Q m₁ * ι Q m₂ ∈ e Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁) (LinearMap.mem_range_self (ι Q) m₂)) #align clifford_algebra.ι_mul_ι_mem_even_odd_zero CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero +-/ +#print CliffordAlgebra.evenOdd_mul_le /- theorem evenOdd_mul_le (i j : ZMod 2) : evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j) := by simp_rw [even_odd, Submodule.iSup_eq_span, Submodule.span_mul_span] @@ -73,31 +84,41 @@ theorem evenOdd_mul_le (i j : ZMod 2) : evenOdd Q i * evenOdd Q j ≤ evenOdd Q simp only [Subtype.coe_mk, Nat.cast_add, pow_add] exact Submodule.mul_mem_mul hx' hy' #align clifford_algebra.even_odd_mul_le CliffordAlgebra.evenOdd_mul_le +-/ +#print CliffordAlgebra.evenOdd.gradedMonoid /- instance evenOdd.gradedMonoid : SetLike.GradedMonoid (evenOdd Q) where one_mem := Submodule.one_le.mp (one_le_evenOdd_zero Q) mul_mem i j p q hp hq := Submodule.mul_le.mp (evenOdd_mul_le Q _ _) _ hp _ hq #align clifford_algebra.even_odd.graded_monoid CliffordAlgebra.evenOdd.gradedMonoid +-/ +#print CliffordAlgebra.GradedAlgebra.ι /- /-- A version of `clifford_algebra.ι` that maps directly into the graded structure. This is primarily an auxiliary construction used to provide `clifford_algebra.graded_algebra`. -/ def GradedAlgebra.ι : M →ₗ[R] ⨁ i : ZMod 2, evenOdd Q i := DirectSum.lof R (ZMod 2) (fun i => ↥(evenOdd Q i)) 1 ∘ₗ (ι Q).codRestrict _ (ι_mem_evenOdd_one Q) #align clifford_algebra.graded_algebra.ι CliffordAlgebra.GradedAlgebra.ι +-/ +#print CliffordAlgebra.GradedAlgebra.ι_apply /- theorem GradedAlgebra.ι_apply (m : M) : GradedAlgebra.ι Q m = DirectSum.of (fun i => ↥(evenOdd Q i)) 1 ⟨ι Q m, ι_mem_evenOdd_one Q m⟩ := rfl #align clifford_algebra.graded_algebra.ι_apply CliffordAlgebra.GradedAlgebra.ι_apply +-/ +#print CliffordAlgebra.GradedAlgebra.ι_sq_scalar /- theorem GradedAlgebra.ι_sq_scalar (m : M) : GradedAlgebra.ι Q m * GradedAlgebra.ι Q m = algebraMap R _ (Q m) := by rw [graded_algebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply] refine' DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _) #align clifford_algebra.graded_algebra.ι_sq_scalar CliffordAlgebra.GradedAlgebra.ι_sq_scalar +-/ +#print CliffordAlgebra.GradedAlgebra.lift_ι_eq /- theorem GradedAlgebra.lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') : lift Q ⟨by apply graded_algebra.ι Q, GradedAlgebra.ι_sq_scalar Q⟩ x' = DirectSum.of (fun i => evenOdd Q i) i' x' := @@ -123,7 +144,9 @@ theorem GradedAlgebra.lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') : apply dfinsupp.single_eq_zero.mpr; rfl · rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl #align clifford_algebra.graded_algebra.lift_ι_eq CliffordAlgebra.GradedAlgebra.lift_ι_eq +-/ +#print CliffordAlgebra.gradedAlgebra /- /-- The clifford algebra is graded by the even and odd parts. -/ instance gradedAlgebra : GradedAlgebra (evenOdd Q) := GradedAlgebra.ofAlgHom (evenOdd Q) @@ -139,7 +162,9 @@ instance gradedAlgebra : GradedAlgebra (evenOdd Q) := rw [lift_ι_apply, graded_algebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]) (by apply graded_algebra.lift_ι_eq Q) #align clifford_algebra.graded_algebra CliffordAlgebra.gradedAlgebra +-/ +#print CliffordAlgebra.iSup_ι_range_eq_top /- theorem iSup_ι_range_eq_top : (⨆ i : ℕ, (ι Q).range ^ i) = ⊤ := by rw [← (DirectSum.Decomposition.isInternal (even_odd Q)).submodule_iSup_eq_top, eq_comm] @@ -150,14 +175,18 @@ theorem iSup_ι_range_eq_top : (⨆ i : ℕ, (ι Q).range ^ i) = ⊤ := _ = ⨆ i : ℕ, (ι Q).range ^ i := Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl #align clifford_algebra.supr_ι_range_eq_top CliffordAlgebra.iSup_ι_range_eq_top +-/ +#print CliffordAlgebra.evenOdd_isCompl /- theorem evenOdd_isCompl : IsCompl (evenOdd Q 0) (evenOdd Q 1) := (DirectSum.Decomposition.isInternal (evenOdd Q)).IsCompl zero_ne_one <| by have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl simpa using congr_arg (coe : Finset (ZMod 2) → Set (ZMod 2)) this #align clifford_algebra.even_odd_is_compl CliffordAlgebra.evenOdd_isCompl +-/ +#print CliffordAlgebra.evenOdd_induction /- /-- To show a property is true on the even or odd part, it suffices to show it is true on the scalars or vectors (respectively), closed under addition, and under left-multiplication by a pair of vectors. -/ @@ -202,7 +231,9 @@ theorem evenOdd_induction (n : ZMod 2) {P : ∀ x, x ∈ evenOdd Q n → Prop} · intro x y hx hy apply hadd #align clifford_algebra.even_odd_induction CliffordAlgebra.evenOdd_induction +-/ +#print CliffordAlgebra.even_induction /- /-- To show a property is true on the even parts, it suffices to show it is true on the scalars, closed under addition, and under left-multiplication by a pair of vectors. -/ @[elab_as_elim] @@ -221,7 +252,9 @@ theorem even_induction {P : ∀ x, x ∈ evenOdd Q 0 → Prop} rintro ⟨r, rfl⟩ exact hr r #align clifford_algebra.even_induction CliffordAlgebra.even_induction +-/ +#print CliffordAlgebra.odd_induction /- /-- To show a property is true on the odd parts, it suffices to show it is true on the vectors, closed under addition, and under left-multiplication by a pair of vectors. -/ @[elab_as_elim] @@ -240,6 +273,7 @@ theorem odd_induction {P : ∀ x, x ∈ evenOdd Q 1 → Prop} rintro ⟨v, rfl⟩ exact hι v #align clifford_algebra.odd_induction CliffordAlgebra.odd_induction +-/ end CliffordAlgebra diff --git a/Mathbin/NumberTheory/Cyclotomic/Discriminant.lean b/Mathbin/NumberTheory/Cyclotomic/Discriminant.lean index f782e5ea26..94a14f5880 100644 --- a/Mathbin/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathbin/NumberTheory/Cyclotomic/Discriminant.lean @@ -36,6 +36,7 @@ variable {n : ℕ+} {K : Type u} [Field K] [CharZero K] {ζ : K} variable [IsCyclotomicExtension {n} ℚ K] +#print IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one /- /-- The discriminant of the power basis given by a primitive root of unity `ζ` is the same as the discriminant of the power basis given by `ζ - 1`. -/ theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) : @@ -55,6 +56,7 @@ theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) : · refine' minpoly.isIntegrallyClosed_eq_field_fractions' _ _ exact isIntegral_sub (hζ.is_integral n.pos) isIntegral_one #align is_primitive_root.discr_zeta_eq_discr_zeta_sub_one IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one +-/ end IsPrimitiveRoot @@ -64,6 +66,7 @@ variable {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Fiel variable [Algebra K L] +#print IsCyclotomicExtension.discr_prime_pow_ne_two /- /-- If `p` is a prime and `is_cyclotomic_extension {p ^ (k + 1)} K L`, then the discriminant of `hζ.power_basis K` is `(-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))` if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/ @@ -126,7 +129,9 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F rw [coe_coe] at h simpa using hne.1 #align is_cyclotomic_extension.discr_prime_pow_ne_two IsCyclotomicExtension.discr_prime_pow_ne_two +-/ +#print IsCyclotomicExtension.discr_prime_pow_ne_two' /- /-- If `p` is a prime and `is_cyclotomic_extension {p ^ (k + 1)} K L`, then the discriminant of `hζ.power_basis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))` if `irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/ @@ -137,7 +142,9 @@ theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : (-1) ^ ((p : ℕ) ^ k * (p - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1)) := by simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk #align is_cyclotomic_extension.discr_prime_pow_ne_two' IsCyclotomicExtension.discr_prime_pow_ne_two' +-/ +#print IsCyclotomicExtension.discr_prime_pow /- /-- If `p` is a prime and `is_cyclotomic_extension {p ^ k} K L`, then the discriminant of `hζ.power_basis K` is `(-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))` if `irreducible (cyclotomic (p ^ k) K))`. Beware that in the cases `p ^ k = 1` and `p ^ k = 2` @@ -183,7 +190,9 @@ theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact ( · exact hcycl · exact discr_prime_pow_ne_two hζ hirr hk #align is_cyclotomic_extension.discr_prime_pow IsCyclotomicExtension.discr_prime_pow +-/ +#print IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow /- /-- If `p` is a prime and `is_cyclotomic_extension {p ^ k} K L`, then there are `u : ℤˣ` and `n : ℕ` such that the discriminant of `hζ.power_basis K` is `u * p ^ n`. Often this is enough and less cumbersome to use than `is_cyclotomic_extension.discr_prime_pow`. -/ @@ -199,7 +208,9 @@ theorem discr_prime_pow_eq_unit_mul_pow [IsCyclotomicExtension {p ^ k} K L] exact ⟨-1, (p : ℕ) ^ (k - 1) * ((p - 1) * k - 1), by simp [(odd_iff_not_even.2 heven).neg_one_pow]⟩ #align is_cyclotomic_extension.discr_prime_pow_eq_unit_mul_pow IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow +-/ +#print IsCyclotomicExtension.discr_odd_prime /- /-- If `p` is an odd prime and `is_cyclotomic_extension {p} K L`, then `discr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)` if `irreducible (cyclotomic p K)`. -/ @@ -216,6 +227,7 @@ theorem discr_odd_prime [IsCyclotomicExtension {p} K L] [hp : Fact (p : ℕ).Pri · rw [zero_add, pow_one, totient_prime hp.out] · rw [pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub] #align is_cyclotomic_extension.discr_odd_prime IsCyclotomicExtension.discr_odd_prime +-/ end IsCyclotomicExtension diff --git a/lake-manifest.json b/lake-manifest.json index ab0f86be95..2d4bc04b37 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,15 +10,15 @@ {"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "9804dc51e2eca47dfe018ca9b9644cc0ced81e4d", + "rev": "d691d1fbb04e99b19a2a009fa5dcd60e555f0ad2", "name": "lean3port", - "inputRev?": "9804dc51e2eca47dfe018ca9b9644cc0ced81e4d"}}, + "inputRev?": "d691d1fbb04e99b19a2a009fa5dcd60e555f0ad2"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "489a04975079ea0399507f81c9035890ca54288a", + "rev": "969f6135c1ad355e99110f61398e551e71433ce5", "name": "mathlib", - "inputRev?": "489a04975079ea0399507f81c9035890ca54288a"}}, + "inputRev?": "969f6135c1ad355e99110f61398e551e71433ce5"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 1152097398..e0967cf2d7 100644 --- a/lakefile.lean +++ b/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-23-05" +def tag : String := "nightly-2023-06-23-07" 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"@"9804dc51e2eca47dfe018ca9b9644cc0ced81e4d" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d691d1fbb04e99b19a2a009fa5dcd60e555f0ad2" @[default_target] lean_lib Mathbin where