Skip to content

Commit 9fdbd11

Browse files
kim-emkim-em
committed
Merge branch 'origin/kim/to-dual-complete-lattice' into kim/to-dual-ccl-extended
2 parents f325d56 + 27536c2 commit 9fdbd11

File tree

40 files changed

+825
-154
lines changed

40 files changed

+825
-154
lines changed

‎.github/workflows/zulip_emoji_ci_status.yaml‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
name: Zulip emoji CI status
2+
3+
on:
4+
workflow_run:
5+
workflows: ["continuous integration", "continuous integration (mathlib forks)"]
6+
types: [requested, completed]
7+
8+
# Limit permissions for GITHUB_TOKEN for the entire workflow
9+
permissions:
10+
contents: read
11+
pull-requests: read
12+
# All other permissions are implicitly 'none'
13+
14+
jobs:
15+
update_ci_emoji:
16+
runs-on: ubuntu-latest
17+
if: github.repository == 'leanprover-community/mathlib4'
18+
steps:
19+
- name: Determine PR number
20+
id: pr
21+
env:
22+
GH_TOKEN: ${{ github.token }}
23+
HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
24+
HEAD_REPO_OWNER: ${{ github.event.workflow_run.head_repository.owner.login }}
25+
HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
26+
run: |
27+
# Try to get PR number from the workflow_run event
28+
PR_NUMBER=$(echo '${{ toJSON(github.event.workflow_run.pull_requests) }}' | jq -r '.[0].number // empty')
29+
# For push-triggered CI (non-fork PRs), pull_requests may be empty;
30+
# fall back to looking up the PR by branch name.
31+
# Use owner:branch format to avoid matching the wrong PR when
32+
# multiple forks use the same branch name.
33+
if [ -z "$PR_NUMBER" ]; then
34+
PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_REPO_OWNER:$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
35+
fi
36+
# If owner-qualified lookup failed, try without owner (for same-repo branches)
37+
if [ -z "$PR_NUMBER" ]; then
38+
PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
39+
fi
40+
if [ -z "$PR_NUMBER" ]; then
41+
echo "No PR found for branch $HEAD_REPO_OWNER:$HEAD_BRANCH at $HEAD_SHA, skipping"
42+
echo "skip=true" >> "$GITHUB_OUTPUT"
43+
else
44+
echo "Found PR #$PR_NUMBER"
45+
echo "pr_number=$PR_NUMBER" >> "$GITHUB_OUTPUT"
46+
echo "skip=false" >> "$GITHUB_OUTPUT"
47+
fi
48+
49+
- name: Determine CI action
50+
id: action
51+
if: steps.pr.outputs.skip != 'true'
52+
run: |
53+
EVENT_ACTION="${{ github.event.action }}"
54+
CONCLUSION="${{ github.event.workflow_run.conclusion }}"
55+
echo "Event action: $EVENT_ACTION, conclusion: $CONCLUSION"
56+
if [ "$EVENT_ACTION" = "requested" ]; then
57+
echo "ci_action=ci-running" >> "$GITHUB_OUTPUT"
58+
elif [ "$EVENT_ACTION" = "completed" ]; then
59+
case "$CONCLUSION" in
60+
success)
61+
echo "ci_action=ci-success" >> "$GITHUB_OUTPUT"
62+
;;
63+
cancelled)
64+
# Clear the running emoji. A new run may or may not follow
65+
# (manual cancel, branch deleted, etc.), so don't leave stale 🟡.
66+
echo "ci_action=ci-cancelled" >> "$GITHUB_OUTPUT"
67+
;;
68+
*)
69+
echo "ci_action=ci-failure" >> "$GITHUB_OUTPUT"
70+
;;
71+
esac
72+
fi
73+
74+
- name: Checkout mathlib repository
75+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
76+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
77+
with:
78+
ref: master
79+
sparse-checkout: |
80+
scripts/zulip_emoji_reactions.py
81+
82+
- name: Set up Python
83+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
84+
uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
85+
with:
86+
python-version: '3.x'
87+
88+
- name: Install dependencies
89+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
90+
run: |
91+
python -m pip install --upgrade pip
92+
pip install zulip
93+
94+
- name: Update CI emoji
95+
if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
96+
env:
97+
ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
98+
ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
99+
ZULIP_SITE: https://leanprover.zulipchat.com
100+
run: |
101+
python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.action.outputs.ci_action }}" "none" "${{ steps.pr.outputs.pr_number }}"

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1373,6 +1373,7 @@ public import Mathlib.AlgebraicGeometry.SpreadingOut
13731373
public import Mathlib.AlgebraicGeometry.Stalk
13741374
public import Mathlib.AlgebraicGeometry.StructureSheaf
13751375
public import Mathlib.AlgebraicGeometry.ValuativeCriterion
1376+
public import Mathlib.AlgebraicGeometry.ZariskisMainTheorem
13761377
public import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
13771378
public import Mathlib.AlgebraicTopology.CechNerve
13781379
public import Mathlib.AlgebraicTopology.DoldKan.Compatibility
@@ -5437,6 +5438,7 @@ public import Mathlib.NumberTheory.NumberField.ClassNumber
54375438
public import Mathlib.NumberTheory.NumberField.Completion
54385439
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
54395440
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
5441+
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
54405442
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
54415443
public import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
54425444
public import Mathlib.NumberTheory.NumberField.Cyclotomic.Three

‎Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Andrew Yang
66
module
77

88
public import Mathlib.AlgebraicGeometry.Artinian
9+
public import Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
910
public import Mathlib.AlgebraicGeometry.Fiber
1011
public import Mathlib.RingTheory.RingHom.QuasiFinite
1112
public import Mathlib.AlgebraicGeometry.Morphisms.Finite
@@ -290,4 +291,48 @@ lemma locallyQuasiFinite_iff_finite_preimage_singleton
290291
LocallyQuasiFinite f ↔ ∀ x, (f ⁻¹' {x}).Finite :=
291292
⟨fun _ ↦ f.finite_preimage_singleton, .of_finite_preimage_singleton f⟩
292293

294+
lemma LocallyQuasiFinite.of_injective {f : X ⟶ Y} [LocallyOfFiniteType f]
295+
(hf : Function.Injective f) : LocallyQuasiFinite f :=
296+
.of_finite_preimage_singleton _ fun _ ↦ (Set.subsingleton_singleton.preimage hf).finite
297+
298+
instance (priority := low) {f : X ⟶ Y} [LocallyOfFiniteType f]
299+
[UniversallyInjective f] : LocallyQuasiFinite f := .of_injective f.injective
300+
301+
/-- A morphism `f : X ⟶ Y` is quasi-finite at `x : X`
302+
if the stalk map `𝒪_{X, x} ⟶ 𝒪_{Y, f x}` is quasi-finite. -/
303+
def Scheme.Hom.QuasiFiniteAt (x : X) : Prop := (f.stalkMap x).hom.QuasiFinite
304+
305+
variable {f} in
306+
lemma Scheme.Hom.QuasiFiniteAt.quasiFiniteAt
307+
{x : X} (hx : f.QuasiFiniteAt x) {V : X.Opens} (hV : IsAffineOpen V) {U : Y.Opens}
308+
(hU : IsAffineOpen U) (hVU : V ≤ f ⁻¹ᵁ U) (hxV : x ∈ V.1) :
309+
(f.appLE U V hVU).hom.QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal := by
310+
algebraize [(f.appLE U V hVU).hom]
311+
have H : (Y.presheaf.germ U _ (hVU hxV)).hom.QuasiFinite := by
312+
algebraize [(Y.presheaf.germ U _ (hVU hxV)).hom]
313+
have := hU.isLocalization_stalk ⟨f x, (hVU hxV)⟩
314+
rw [← (Y.presheaf.germ U _ (hVU hxV)).hom.algebraMap_toAlgebra,
315+
RingHom.quasiFinite_algebraMap]
316+
exact .of_isLocalization (hU.primeIdealOf ⟨_, hVU hxV⟩).asIdeal.primeCompl
317+
algebraize [(X.presheaf.germ V x hxV).hom]
318+
have := hV.isLocalization_stalk ⟨x, hxV⟩
319+
let e := IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hxV⟩).asIdeal.primeCompl
320+
(X.presheaf.stalk (⟨x, hxV⟩ : V.1)) (Localization.AtPrime (hV.primeIdealOf ⟨x, hxV⟩).asIdeal)
321+
rw [RingHom.QuasiFiniteAt, Algebra.QuasiFiniteAt, ← RingHom.quasiFinite_algebraMap]
322+
convert (RingHom.QuasiFinite.of_finite e.finite).comp (hx.comp H)
323+
rw [← CommRingCat.hom_comp, f.germ_stalkMap, ← X.presheaf.germ_res (homOfLE hVU) _ hxV,
324+
Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map_assoc, CommRingCat.hom_comp, ← RingHom.comp_assoc,
325+
IsScalarTower.algebraMap_eq Γ(Y, U) Γ(X, V), e.toAlgHom.comp_algebraMap.symm]
326+
rfl
327+
328+
lemma Scheme.Hom.quasiFiniteAt [LocallyQuasiFinite f] (x : X) :
329+
f.QuasiFiniteAt x := by
330+
refine HasRingHomProperty.stalkMap ?_ ‹_› x
331+
introv hf
332+
algebraize [f]
333+
refine .of_comp (g := algebraMap R _) ?_
334+
convert RingHom.quasiFinite_algebraMap.mpr (inferInstanceAs
335+
(Algebra.QuasiFinite R (Localization.AtPrime J)))
336+
ext; simp; rfl
337+
293338
end AlgebraicGeometry

0 commit comments

Comments
 (0)
⚡