Continuous algebra Map of density
continuous_algebraMap_of_density
Plain-language statement
Maddy's Lemma : Density implies continuity.
Exact Lean statement
@[fun_prop] lemma continuous_algebraMap_of_density :
Continuous (algebraMap K L)Formal artifact
Lean source
@[fun_prop] lemma continuous_algebraMap_of_density : Continuous (algebraMap K L) := by apply continuous_of_continuousAt_zero _ _ simp only [ContinuousAt, map_zero] have B₁ := IsValuativeTopology.hasBasis_nhds_zero K have B₂ := IsValuativeTopology.hasBasis_nhds_zero L apply (Filter.HasBasis.tendsto_iff B₁ B₂).mpr simp only [Set.mem_ofPred_eq, true_and, true_imp_iff] intro b obtain ⟨a, rfl⟩ := unitsMap_valuation_surjective b obtain ⟨a', ha'⟩ := exists_valuation_algebraMap_le_valuation K a refine ⟨a'.map (valuation K), fun x hx ↦ ?_⟩ simp only [Units.coe_map, MonoidHom.coe_coe] at hx ⊢ exact lt_of_lt_of_le (ValuativeExtension.algebraMap_lt.mpr hx) ha'- Project
- Class Field Theory
- License
- Apache-2.0
- Commit
- f18cd7fd1575
- Source
- ClassFieldTheory/LocalCFT/Continuity.lean:94-107
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Exists valuation algebra Map eq valuation pow
exists_valuation_algebraMap_eq_valuation_pow
Plain-language statement
Andrew's Lemma : Density for algebraic extensions.
Source project: Class Field Theory
Person-level attribution pending.
Exists of surjective
groupCohomology.exists_of_surjective
Plain-language statement
Given map f: M ⟶ N and q : ℕ, if H^{q+1}(M) ⟶ H^{q+1}(N) is surjective, then any z : Z^{q+1}(N) can be written as f(z') + d(y) for some z' : Z^{q+1}(M) and y : C^q(M). Note that d is spelled as toCocycles.
Source project: Class Field Theory
Person-level attribution pending.
Infl δ naturality
groupCohomology.infl_δ_naturality
Plain-language statement
Assume that we have a short exact sequence 0 → A → B → C → 0 in Rep R G and that the sequence of H- invariants is also a short exact in Rep R (G ⧸ H) : 0 → Aᴴ → Bᴴ → Cᴴ → 0. Then we have a commuting square Hⁿ(G ⧸ H, Cᴴ) ⟶ H^{n+1}(G ⧸ H, Aᴴ) | | ↓ ↓ Hⁿ(G , C) ⟶ H^{n+1}(G,A) where the horizontal maps are connecting homomorphisms an...
Source project: Class Field Theory
Person-level attribution pending.